Theorem prid1 4701

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  prid2  4702  prnz  4716  preq12b  4788  unisn2  5241  opi1  5415  opeluu  5417  dmrnssfld  5923  funopg  6526  fprb  7145  fveqf1o  7253  2dom  8974  dif1en  9093  opthreg  9537  djuss  9842  dfac2b  10051  brdom7disj  10451  brdom6disj  10452  reelprrecn  11128  pnfxr  11197  m1expcl2  14045  hash2prb  14432  sadcf  16420  prmreclem2  16886  fnpr2ob  17520  setcepi  18053  setc2obas  18059  setc2ohom  18060  cat1  18062  grpss  18928  efgi0  19693  vrgpf  19741  vrgpinv  19742  frgpuptinv  19744  frgpup2  19749  frgpnabllem1  19846  dmdprdpr  20024  dprdpr  20025  cnmsgnsubg  21559  m2detleiblem5  22615  m2detleiblem3  22619  m2detleiblem4  22620  m2detleib  22621  indistopon  22991  indiscld  23081  xpstopnlem1  23799  xpstopnlem2  23801  xpsdsval  24371  ehl2eudis  25414  i1f1lem  25681  i1f1  25682  dvnfre  25944  c1lip2  25990  aannenlem2  26320  cxplogb  26775  ppiublem2  27191  lgsdir2lem3  27315  noxp1o  27652  noextendlt  27658  nosepdmlem  27672  nolt02o  27684  nosupbnd1lem5  27701  nosupbnd2lem1  27704  noinfno  27707  noinfbnd1  27718  noinfbnd2lem1  27719  noetasuplem1  27722  eengbas  29075  ebtwntg  29076  structvtxval  29115  usgr2trlncl  29853  usgrwwlks2on  30051  umgrwwlks2on  30052  wlk2v2e  30252  eulerpathpr  30335  s2rnOLD  33030  psgnid  33185  trsp2cyc  33211  cyc3fv1  33225  cnmsgn0g  33234  constr01  33933  constrss  33934  constrconj  33936  constrelextdg2  33938  nn0constr  33952  prsiga  34322  coinflippvt  34676  subfacp1lem3  35417  kur14lem7  35447  ex-sategoelel12  35662  onint1  36684  poimirlem22  38016  pw2f1ocnv  43489  2omomeqom  43755  omcl3g  43786  fvrcllb0d  44144  fvrcllb0da  44145  corclrcl  44158  relexp0idm  44166  corcltrcl  44190  mnuprdlem1  44723  mnuprdlem3  44725  mnurndlem1  44732  nregmodellem  45467  refsum2cnlem1  45492  limsup10exlem  46222  fourierdlem103  46659  fourierdlem104  46660  prsal  46768  usgrgrtrirex  48448  stgr1  48459  stgrnbgr0  48462  grlimgrtrilem1  48499  gpgiedgdmellem  48544  gpgvtx0  48551  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem9  48601  zlmodzxzscm  48855  zlmodzxzldeplem3  49000  2arympt  49147  rrx2pxel  49209  rrx2linesl  49241  2sphere0  49248  setc1onsubc  50099