Theorem prid1g 4761

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)

Assertion

Ref	Expression
prid1g	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Proof of Theorem prid1g

Step	Hyp	Ref	Expression
1		eqid 2728	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 864	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4646	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1534   ∈ wcel 2099  {cpr 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-un 3950  df-sn 4626  df-pr 4628

This theorem is referenced by:  prid2g  4762  prid1  4763  prnzg  4779  preq1b  4844  prel12g  4861  elpreqprb  4865  prproe  4902  opth1  5472  fr2nr  5651  fpr2g  7218  f1prex  7288  fveqf1o  7307  pw2f1olem  9095  hashprdifel  14384  gcdcllem3  16470  mgm2nsgrplem1  18864  mgm2nsgrplem2  18865  mgm2nsgrplem3  18866  sgrp2nmndlem1  18869  sgrp2rid2  18872  pmtrprfv  19402  pptbas  22905  coseq0negpitopi  26432  uhgr2edg  29015  umgrvad2edg  29020  uspgr2v1e2w  29058  usgr2v1e2w  29059  nbusgredgeu0  29175  nbusgrf1o0  29176  nb3grprlem1  29187  nb3grprlem2  29188  vtxduhgr0nedg  29300  1hegrvtxdg1  29315  1egrvtxdg1  29317  umgr2v2evd2  29335  vdegp1bi  29345  mptprop  32473  altgnsg  32865  cyc3genpmlem  32867  elrspunsn  33140  bj-prmoore  36589  ftc1anclem8  37168  kelac2  42480  pr2el1  42970  pr2eldif1  42975  fourierdlem54  45539  sge0pr  45773  imarnf1pr  46653  paireqne  46842  fmtnoprmfac2lem1  46897  1hegrlfgr  47185