Theorem prid1 4729

Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 24-Jun-1993.)

Hypothesis

Ref	Expression
prid1.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
prid1	⊢ 𝐴 ∈ {𝐴, 𝐵}

Proof of Theorem prid1

Step	Hyp	Ref	Expression
1		prid1.1	. 2 ⊢ 𝐴 ∈ V
2		prid1g 4727	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2143  Vcvv 3455  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  prid2  4730  prnz  4744  preq12b  4816  unisn2  5276  opi1  5452  opeluu  5454  dmrnssfld  5966  funopg  6572  fprb  7194  fveqf1o  7302  2dom  9028  dif1en  9147  opthreg  9588  djuss  9907  dfac2b  10115  brdom7disj  10516  brdom6disj  10517  reelprrecn  11193  0elpr01  11202  pnfxr  11264  m1expcl2  14123  hash2prb  14511  sadcf  16512  fnpr2ob  17613  setcepi  18146  setc2obas  18152  setc2ohom  18153  cat1  18155  grpss  19022  efgi0  19791  vrgpf  19839  vrgpinv  19840  frgpuptinv  19842  frgpup2  19847  frgpnabllem1  19944  dmdprdpr  20122  dprdpr  20123  cnmsgnsubg  21708  m2detleiblem5  22763  m2detleiblem3  22767  m2detleiblem4  22768  m2detleib  22769  indistopon  23139  indiscld  23229  xpstopnlem1  23947  xpstopnlem2  23949  xpsdsval  24519  ehl2eudis  25562  dvnfre  26092  c1lip2  26138  aannenlem2  26473  ppiublem2  27348  lgsdir2lem3  27472  noxp1o  27808  noextendlt  27814  nosepdmlem  27828  nolt02o  27840  nosupbnd1lem5  27857  nosupbnd2lem1  27860  noinfno  27863  noinfbnd1  27874  noinfbnd2lem1  27875  noetasuplem1  27878  eengbas  29312  ebtwntg  29313  structvtxval  29352  wlk2v2e  30489  eulerpathpr  30572  s2rnOLD  33245  psgnid  33398  trsp2cyc  33424  cnmsgn0g  33447  prsiga  34502  coinflippvt  34856  subfacp1lem3  35655  kur14lem7  35685  ex-sategoelel12  35900  onint1  36941  poimirlem22  38274  pw2f1ocnv  43747  2omomeqom  44013  omcl3g  44044  relexp0idm  44424  corcltrcl  44448  mnuprdlem1  44965  mnuprdlem3  44967  mnurndlem1  44974  nregmodellem  45708  refsum2cnlem1  45740  fourierdlem103  46906  fourierdlem104  46907  prsal  47015  usgrgrtrirex  48698  stgrnbgr0  48712  grlimgrtrilem1  48749  zlmodzxzldeplem3  49265  rrx2pxel  49474  rrx2linesl  49506  2sphere0  49513  setc1onsubc  50363