Theorem prid1g 4696

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

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1539   ∈ wcel 2106  {cpr 4563

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  prid2g  4697  prid1  4698  prnzg  4714  preq1b  4777  prel12g  4794  elpreqprb  4798  prproe  4837  opth1  5390  fr2nr  5567  fpr2g  7087  f1prex  7156  fveqf1o  7175  pw2f1olem  8863  hashprdifel  14113  gcdcllem3  16208  mgm2nsgrplem1  18557  mgm2nsgrplem2  18558  mgm2nsgrplem3  18559  sgrp2nmndlem1  18562  sgrp2rid2  18565  pmtrprfv  19061  pptbas  22158  coseq0negpitopi  25660  uhgr2edg  27575  umgrvad2edg  27580  uspgr2v1e2w  27618  usgr2v1e2w  27619  nbusgredgeu0  27735  nbusgrf1o0  27736  nb3grprlem1  27747  nb3grprlem2  27748  vtxduhgr0nedg  27859  1hegrvtxdg1  27874  1egrvtxdg1  27876  umgr2v2evd2  27894  vdegp1bi  27904  mptprop  31031  altgnsg  31416  cyc3genpmlem  31418  bj-prmoore  35286  ftc1anclem8  35857  kelac2  40890  pr2el1  41156  pr2eldif1  41161  fourierdlem54  43701  sge0pr  43932  imarnf1pr  44774  paireqne  44963  fmtnoprmfac2lem1  45018  1hegrlfgr  45294