Theorem prid1 4695

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 4693	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ {𝐴, 𝐵}

Syntax hints:   ∈ wcel 2108  Vcvv 3422  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  prid2  4696  prnz  4710  preq12b  4778  unisn2  5231  opi1  5377  opeluu  5379  dmrnssfld  5868  funopg  6452  fprb  7051  fveqf1o  7155  2dom  8774  dif1en  8907  opthreg  9306  djuss  9609  dfac2b  9817  brdom7disj  10218  brdom6disj  10219  reelprrecn  10894  pnfxr  10960  m1expcl2  13732  hash2prb  14114  sadcf  16088  prmreclem2  16546  fnpr2ob  17186  setcepi  17719  setc2obas  17725  setc2ohom  17726  cat1  17728  grpss  18512  efgi0  19241  vrgpf  19289  vrgpinv  19290  frgpuptinv  19292  frgpup2  19297  frgpnabllem1  19389  dmdprdpr  19567  dprdpr  19568  cnmsgnsubg  20694  m2detleiblem5  21682  m2detleiblem3  21686  m2detleiblem4  21687  m2detleib  21688  indistopon  22059  indiscld  22150  xpstopnlem1  22868  xpstopnlem2  22870  xpsdsval  23442  ehl2eudis  24491  i1f1lem  24758  i1f1  24759  dvnfre  25021  c1lip2  25067  aannenlem2  25394  cxplogb  25841  ppiublem2  26256  lgsdir2lem3  26380  eengbas  27252  ebtwntg  27253  structvtxval  27294  usgr2trlncl  28029  umgrwwlks2on  28223  wlk2v2e  28422  eulerpathpr  28505  s2rn  31120  psgnid  31266  trsp2cyc  31292  cyc3fv1  31306  cnmsgn0g  31315  prsiga  31999  coinflippvt  32351  subfacp1lem3  33044  kur14lem7  33074  ex-sategoelel12  33289  noxp1o  33793  noextendlt  33799  nosepdmlem  33813  nolt02o  33825  nosupbnd1lem5  33842  nosupbnd2lem1  33845  noinfno  33848  noinfbnd1  33859  noinfbnd2lem1  33860  noetasuplem1  33863  onint1  34565  poimirlem22  35726  pw2f1ocnv  40775  fvrcllb0d  41190  fvrcllb0da  41191  corclrcl  41204  relexp0idm  41212  corcltrcl  41236  mnuprdlem1  41779  mnuprdlem3  41781  mnurndlem1  41788  refsum2cnlem1  42469  limsup10exlem  43203  fourierdlem103  43640  fourierdlem104  43641  prsal  43749  zlmodzxzscm  45581  zlmodzxzldeplem3  45731  2arympt  45883  rrx2pxel  45945  rrx2linesl  45977  2sphere0  45984