Theorem prid1 4721

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  {cpr 4584

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  prid2  4722  prnz  4736  preq12b  4808  unisn2  5259  opi1  5424  opeluu  5426  dmrnssfld  5931  funopg  6534  fprb  7150  fveqf1o  7258  2dom  8979  dif1en  9098  opthreg  9539  djuss  9844  dfac2b  10053  brdom7disj  10453  brdom6disj  10454  reelprrecn  11130  pnfxr  11198  m1expcl2  14020  hash2prb  14407  sadcf  16392  prmreclem2  16857  fnpr2ob  17491  setcepi  18024  setc2obas  18030  setc2ohom  18031  cat1  18033  grpss  18896  efgi0  19661  vrgpf  19709  vrgpinv  19710  frgpuptinv  19712  frgpup2  19717  frgpnabllem1  19814  dmdprdpr  19992  dprdpr  19993  cnmsgnsubg  21544  m2detleiblem5  22581  m2detleiblem3  22585  m2detleiblem4  22586  m2detleib  22587  indistopon  22957  indiscld  23047  xpstopnlem1  23765  xpstopnlem2  23767  xpsdsval  24337  ehl2eudis  25390  i1f1lem  25658  i1f1  25659  dvnfre  25924  c1lip2  25971  aannenlem2  26305  cxplogb  26764  ppiublem2  27182  lgsdir2lem3  27306  noxp1o  27643  noextendlt  27649  nosepdmlem  27663  nolt02o  27675  nosupbnd1lem5  27692  nosupbnd2lem1  27695  noinfno  27698  noinfbnd1  27709  noinfbnd2lem1  27710  noetasuplem1  27713  eengbas  29066  ebtwntg  29067  structvtxval  29106  usgr2trlncl  29845  usgrwwlks2on  30043  umgrwwlks2on  30044  wlk2v2e  30244  eulerpathpr  30327  s2rnOLD  33036  psgnid  33190  trsp2cyc  33216  cyc3fv1  33230  cnmsgn0g  33239  constr01  33919  constrss  33920  constrconj  33922  constrelextdg2  33924  nn0constr  33938  prsiga  34308  coinflippvt  34662  subfacp1lem3  35395  kur14lem7  35425  ex-sategoelel12  35640  onint1  36662  poimirlem22  37890  pw2f1ocnv  43391  2omomeqom  43657  omcl3g  43688  fvrcllb0d  44046  fvrcllb0da  44047  corclrcl  44060  relexp0idm  44068  corcltrcl  44092  mnuprdlem1  44625  mnuprdlem3  44627  mnurndlem1  44634  nregmodellem  45369  refsum2cnlem1  45394  limsup10exlem  46127  fourierdlem103  46564  fourierdlem104  46565  prsal  46673  usgrgrtrirex  48307  stgr1  48318  stgrnbgr0  48321  grlimgrtrilem1  48358  gpgiedgdmellem  48403  gpgvtx0  48410  gpgprismgr4cycllem3  48454  gpgprismgr4cycllem9  48460  zlmodzxzscm  48714  zlmodzxzldeplem3  48859  2arympt  49006  rrx2pxel  49068  rrx2linesl  49100  2sphere0  49107  setc1onsubc  49958