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 2109  Vcvv 3450  {cpr 4594

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  prid2  4730  prnz  4744  preq12b  4817  unisn2  5270  opi1  5431  opeluu  5433  dmrnssfld  5940  funopg  6553  fprb  7171  fveqf1o  7280  2dom  9004  dif1en  9130  dif1enOLD  9132  opthreg  9578  djuss  9880  dfac2b  10091  brdom7disj  10491  brdom6disj  10492  reelprrecn  11167  pnfxr  11235  m1expcl2  14057  hash2prb  14444  sadcf  16430  prmreclem2  16895  fnpr2ob  17528  setcepi  18057  setc2obas  18063  setc2ohom  18064  cat1  18066  grpss  18893  efgi0  19657  vrgpf  19705  vrgpinv  19706  frgpuptinv  19708  frgpup2  19713  frgpnabllem1  19810  dmdprdpr  19988  dprdpr  19989  cnmsgnsubg  21493  m2detleiblem5  22519  m2detleiblem3  22523  m2detleiblem4  22524  m2detleib  22525  indistopon  22895  indiscld  22985  xpstopnlem1  23703  xpstopnlem2  23705  xpsdsval  24276  ehl2eudis  25329  i1f1lem  25597  i1f1  25598  dvnfre  25863  c1lip2  25910  aannenlem2  26244  cxplogb  26703  ppiublem2  27121  lgsdir2lem3  27245  noxp1o  27582  noextendlt  27588  nosepdmlem  27602  nolt02o  27614  nosupbnd1lem5  27631  nosupbnd2lem1  27634  noinfno  27637  noinfbnd1  27648  noinfbnd2lem1  27649  noetasuplem1  27652  eengbas  28915  ebtwntg  28916  structvtxval  28955  usgr2trlncl  29697  umgrwwlks2on  29894  wlk2v2e  30093  eulerpathpr  30176  s2rnOLD  32872  psgnid  33061  trsp2cyc  33087  cyc3fv1  33101  cnmsgn0g  33110  constr01  33739  constrss  33740  constrconj  33742  constrelextdg2  33744  nn0constr  33758  prsiga  34128  coinflippvt  34483  subfacp1lem3  35176  kur14lem7  35206  ex-sategoelel12  35421  onint1  36444  poimirlem22  37643  pw2f1ocnv  43033  2omomeqom  43299  omcl3g  43330  fvrcllb0d  43689  fvrcllb0da  43690  corclrcl  43703  relexp0idm  43711  corcltrcl  43735  mnuprdlem1  44268  mnuprdlem3  44270  mnurndlem1  44277  nregmodellem  45013  refsum2cnlem1  45038  limsup10exlem  45777  fourierdlem103  46214  fourierdlem104  46215  prsal  46323  usgrgrtrirex  47953  stgr1  47964  stgrnbgr0  47967  grlimgrtrilem1  47997  gpgiedgdmellem  48041  gpgvtx0  48048  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem9  48097  zlmodzxzscm  48349  zlmodzxzldeplem3  48495  2arympt  48642  rrx2pxel  48704  rrx2linesl  48736  2sphere0  48743  setc1onsubc  49595