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 ⊢ 𝐴 ∈ {𝐴, 𝐵}

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  {cpr 4596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  prid2  4734  prnz  4748  preq12b  4820  unisn2  5280  opi1  5455  opeluu  5457  dmrnssfld  5969  funopg  6577  fprb  7199  fveqf1o  7311  2dom  9037  dif1en  9156  opthreg  9597  djuss  9925  dfac2b  10133  brdom7disj  10533  brdom6disj  10534  reelprrecn  11210  0elpr01  11219  pnfxr  11281  m1expcl2  14141  hash2prb  14529  sadcf  16536  fnpr2ob  17637  setcepi  18170  setc2obas  18176  setc2ohom  18177  cat1  18179  grpss  19052  efgi0  19821  vrgpf  19869  vrgpinv  19870  frgpuptinv  19872  frgpup2  19877  frgpnabllem1  19974  dmdprdpr  20152  dprdpr  20153  cnmsgnsubg  21764  m2detleiblem5  22819  m2detleiblem3  22823  m2detleiblem4  22824  m2detleib  22825  indistopon  23195  indiscld  23285  xpstopnlem1  24003  xpstopnlem2  24005  xpsdsval  24575  ehl2eudis  25618  dvnfre  26148  c1lip2  26194  aannenlem2  26529  ppiublem2  27404  lgsdir2lem3  27528  noxp1o  27864  noextendlt  27870  nosepdmlem  27884  nolt02o  27896  nosupbnd1lem5  27913  nosupbnd2lem1  27916  noinfno  27919  noinfbnd1  27930  noinfbnd2lem1  27931  noetasuplem1  27934  eengbas  29368  ebtwntg  29369  structvtxval  29408  wlk2v2e  30545  eulerpathpr  30628  psgnid  33448  trsp2cyc  33474  cnmsgn0g  33497  prsiga  34552  coinflippvt  34907  subfacp1lem3  35695  kur14lem7  35725  ex-sategoelel12  35940  onint1  37001  poimirlem22  38334  pw2f1ocnv  43805  2omomeqom  44071  omcl3g  44102  relexp0idm  44482  corcltrcl  44506  mnuprdlem1  45023  mnuprdlem3  45025  mnurndlem1  45032  nregmodellem  45766  refsum2cnlem1  45798  fourierdlem103  46964  fourierdlem104  46965  prsal  47073  usgrgrtrirex  48756  stgrnbgr0  48770  grlimgrtrilem1  48807  zlmodzxzldeplem3  49323  rrx2pxel  49532  rrx2linesl  49564  2sphere0  49571  setc1onsubc  50421