Theorem prid1g 4763

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 2732	. . 3 ⊢ 𝐴 = 𝐴
2	1	orci 863	. 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)
3		elprg 4648	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵)))
4	2, 3	mpbiri 257	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1541   ∈ wcel 2106  {cpr 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-sn 4628  df-pr 4630

This theorem is referenced by:  prid2g  4764  prid1  4765  prnzg  4781  preq1b  4846  prel12g  4863  elpreqprb  4867  prproe  4905  opth1  5474  fr2nr  5653  fpr2g  7209  f1prex  7278  fveqf1o  7297  pw2f1olem  9072  hashprdifel  14354  gcdcllem3  16438  mgm2nsgrplem1  18795  mgm2nsgrplem2  18796  mgm2nsgrplem3  18797  sgrp2nmndlem1  18800  sgrp2rid2  18803  pmtrprfv  19315  pptbas  22502  coseq0negpitopi  26004  uhgr2edg  28454  umgrvad2edg  28459  uspgr2v1e2w  28497  usgr2v1e2w  28498  nbusgredgeu0  28614  nbusgrf1o0  28615  nb3grprlem1  28626  nb3grprlem2  28627  vtxduhgr0nedg  28738  1hegrvtxdg1  28753  1egrvtxdg1  28755  umgr2v2evd2  28773  vdegp1bi  28783  mptprop  31907  altgnsg  32295  cyc3genpmlem  32297  elrspunsn  32535  bj-prmoore  35984  ftc1anclem8  36556  kelac2  41792  pr2el1  42285  pr2eldif1  42290  fourierdlem54  44862  sge0pr  45096  imarnf1pr  45976  paireqne  46165  fmtnoprmfac2lem1  46220  1hegrlfgr  46496