Theorem prid1 4715

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  prid2  4716  prnz  4730  preq12b  4802  unisn2  5250  opi1  5408  opeluu  5410  dmrnssfld  5913  funopg  6515  fprb  7128  fveqf1o  7236  2dom  8952  dif1en  9071  opthreg  9508  djuss  9813  dfac2b  10022  brdom7disj  10422  brdom6disj  10423  reelprrecn  11098  pnfxr  11166  m1expcl2  13992  hash2prb  14379  sadcf  16364  prmreclem2  16829  fnpr2ob  17462  setcepi  17995  setc2obas  18001  setc2ohom  18002  cat1  18004  grpss  18867  efgi0  19633  vrgpf  19681  vrgpinv  19682  frgpuptinv  19684  frgpup2  19689  frgpnabllem1  19786  dmdprdpr  19964  dprdpr  19965  cnmsgnsubg  21515  m2detleiblem5  22541  m2detleiblem3  22545  m2detleiblem4  22546  m2detleib  22547  indistopon  22917  indiscld  23007  xpstopnlem1  23725  xpstopnlem2  23727  xpsdsval  24297  ehl2eudis  25350  i1f1lem  25618  i1f1  25619  dvnfre  25884  c1lip2  25931  aannenlem2  26265  cxplogb  26724  ppiublem2  27142  lgsdir2lem3  27266  noxp1o  27603  noextendlt  27609  nosepdmlem  27623  nolt02o  27635  nosupbnd1lem5  27652  nosupbnd2lem1  27655  noinfno  27658  noinfbnd1  27669  noinfbnd2lem1  27670  noetasuplem1  27673  eengbas  28960  ebtwntg  28961  structvtxval  29000  usgr2trlncl  29739  umgrwwlks2on  29936  wlk2v2e  30135  eulerpathpr  30218  s2rnOLD  32923  psgnid  33064  trsp2cyc  33090  cyc3fv1  33104  cnmsgn0g  33113  constr01  33753  constrss  33754  constrconj  33756  constrelextdg2  33758  nn0constr  33772  prsiga  34142  coinflippvt  34496  subfacp1lem3  35224  kur14lem7  35254  ex-sategoelel12  35469  onint1  36489  poimirlem22  37688  pw2f1ocnv  43076  2omomeqom  43342  omcl3g  43373  fvrcllb0d  43732  fvrcllb0da  43733  corclrcl  43746  relexp0idm  43754  corcltrcl  43778  mnuprdlem1  44311  mnuprdlem3  44313  mnurndlem1  44320  nregmodellem  45055  refsum2cnlem1  45080  limsup10exlem  45816  fourierdlem103  46253  fourierdlem104  46254  prsal  46362  usgrgrtrirex  47987  stgr1  47998  stgrnbgr0  48001  grlimgrtrilem1  48038  gpgiedgdmellem  48083  gpgvtx0  48090  gpgprismgr4cycllem3  48134  gpgprismgr4cycllem9  48140  zlmodzxzscm  48394  zlmodzxzldeplem3  48540  2arympt  48687  rrx2pxel  48749  rrx2linesl  48781  2sphere0  48788  setc1onsubc  49640