Theorem prid1 4733

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  prid2  4734  prnz  4748  preq12b  4819  unisn2  5277  opi1  5451  opeluu  5453  dmrnssfld  5965  funopg  6571  fprb  7193  fveqf1o  7301  2dom  9027  dif1en  9146  opthreg  9587  djuss  9906  dfac2b  10114  brdom7disj  10515  brdom6disj  10516  reelprrecn  11192  0elpr01  11201  pnfxr  11263  m1expcl2  14121  hash2prb  14509  sadcf  16511  prmreclem2  16977  fnpr2ob  17612  setcepi  18145  setc2obas  18151  setc2ohom  18152  cat1  18154  grpss  19021  efgi0  19790  vrgpf  19838  vrgpinv  19839  frgpuptinv  19841  frgpup2  19846  frgpnabllem1  19943  dmdprdpr  20121  dprdpr  20122  cnmsgnsubg  21696  m2detleiblem5  22751  m2detleiblem3  22755  m2detleiblem4  22756  m2detleib  22757  indistopon  23127  indiscld  23217  xpstopnlem1  23935  xpstopnlem2  23937  xpsdsval  24507  ehl2eudis  25550  i1f1lem  25817  i1f1  25818  dvnfre  26080  c1lip2  26126  aannenlem2  26459  cxplogb  26917  ppiublem2  27333  lgsdir2lem3  27457  noxp1o  27793  noextendlt  27799  nosepdmlem  27813  nolt02o  27825  nosupbnd1lem5  27842  nosupbnd2lem1  27845  noinfno  27848  noinfbnd1  27859  noinfbnd2lem1  27860  noetasuplem1  27863  eengbas  29272  ebtwntg  29273  structvtxval  29312  usgr2trlncl  30050  usgrwwlks2on  30248  umgrwwlks2on  30249  wlk2v2e  30449  eulerpathpr  30532  s2rnOLD  33205  psgnid  33358  trsp2cyc  33384  cyc3fv1  33398  cnmsgn0g  33407  constr01  34077  constrss  34078  constrelextdg2  34082  nn0constr  34096  prsiga  34466  coinflippvt  34820  subfacp1lem3  35573  kur14lem7  35603  ex-sategoelel12  35818  onint1  36849  poimirlem22  38181  pw2f1ocnv  43656  2omomeqom  43922  omcl3g  43953  fvrcllb0d  44311  fvrcllb0da  44312  corclrcl  44325  relexp0idm  44333  corcltrcl  44357  mnuprdlem1  44874  mnuprdlem3  44876  mnurndlem1  44883  nregmodellem  45617  refsum2cnlem1  45649  limsup10exlem  46378  fourierdlem103  46815  fourierdlem104  46816  prsal  46924  usgrgrtrirex  48604  stgr1  48615  stgrnbgr0  48618  grlimgrtrilem1  48655  gpgiedgdmellem  48700  gpgvtx0  48707  gpgprismgr4cycllem3  48751  gpgprismgr4cycllem9  48757  zlmodzxzscm  49022  zlmodzxzldeplem3  49167  2arympt  49314  rrx2pxel  49376  rrx2linesl  49408  2sphere0  49415  setc1onsubc  50265