Theorem prid1 4738

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  prid2  4739  prnz  4753  preq12b  4826  unisn2  5282  opi1  5443  opeluu  5445  dmrnssfld  5953  funopg  6570  fprb  7186  fveqf1o  7295  2dom  9044  dif1en  9174  dif1enOLD  9176  opthreg  9632  djuss  9934  dfac2b  10145  brdom7disj  10545  brdom6disj  10546  reelprrecn  11221  pnfxr  11289  m1expcl2  14103  hash2prb  14490  sadcf  16472  prmreclem2  16937  fnpr2ob  17572  setcepi  18101  setc2obas  18107  setc2ohom  18108  cat1  18110  grpss  18937  efgi0  19701  vrgpf  19749  vrgpinv  19750  frgpuptinv  19752  frgpup2  19757  frgpnabllem1  19854  dmdprdpr  20032  dprdpr  20033  cnmsgnsubg  21537  m2detleiblem5  22563  m2detleiblem3  22567  m2detleiblem4  22568  m2detleib  22569  indistopon  22939  indiscld  23029  xpstopnlem1  23747  xpstopnlem2  23749  xpsdsval  24320  ehl2eudis  25374  i1f1lem  25642  i1f1  25643  dvnfre  25908  c1lip2  25955  aannenlem2  26289  cxplogb  26748  ppiublem2  27166  lgsdir2lem3  27290  noxp1o  27627  noextendlt  27633  nosepdmlem  27647  nolt02o  27659  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfno  27682  noinfbnd1  27693  noinfbnd2lem1  27694  noetasuplem1  27697  eengbas  28960  ebtwntg  28961  structvtxval  29000  usgr2trlncl  29742  umgrwwlks2on  29939  wlk2v2e  30138  eulerpathpr  30221  s2rnOLD  32919  psgnid  33108  trsp2cyc  33134  cyc3fv1  33148  cnmsgn0g  33157  constr01  33776  constrss  33777  constrconj  33779  constrelextdg2  33781  nn0constr  33795  prsiga  34162  coinflippvt  34517  subfacp1lem3  35204  kur14lem7  35234  ex-sategoelel12  35449  onint1  36467  poimirlem22  37666  pw2f1ocnv  43061  2omomeqom  43327  omcl3g  43358  fvrcllb0d  43717  fvrcllb0da  43718  corclrcl  43731  relexp0idm  43739  corcltrcl  43763  mnuprdlem1  44296  mnuprdlem3  44298  mnurndlem1  44305  refsum2cnlem1  45061  limsup10exlem  45801  fourierdlem103  46238  fourierdlem104  46239  prsal  46347  usgrgrtrirex  47962  stgr1  47973  stgrnbgr0  47976  grlimgrtrilem1  48006  gpgiedgdmellem  48050  gpgvtx0  48057  gpgprismgr4cycllem3  48096  gpgprismgr4cycllem9  48102  zlmodzxzscm  48332  zlmodzxzldeplem3  48478  2arympt  48629  rrx2pxel  48691  rrx2linesl  48723  2sphere0  48730  setc1onsubc  49479