Theorem prid1 4611

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

Syntax hints:   ∈ wcel 2083  Vcvv 3440  {cpr 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-un 3870  df-sn 4479  df-pr 4481

This theorem is referenced by:  prid2  4612  prnz  4625  preq12b  4694  unisn2  5114  opi1  5259  opeluu  5261  dmrnssfld  5729  funopg  6266  fprb  6830  fveqf1o  6930  2dom  8437  opthreg  8934  djuss  9202  dfac2b  9409  brdom7disj  9806  brdom6disj  9807  reelprrecn  10482  pnfxr  10548  m1expcl2  13305  hash2prb  13680  sadcf  15639  prmreclem2  16086  fnpr2ob  16664  setcepi  17181  grpss  17883  efgi0  18577  vrgpf  18625  vrgpinv  18626  frgpuptinv  18628  frgpup2  18633  frgpnabllem1  18720  dmdprdpr  18892  dprdpr  18893  cnmsgnsubg  20407  m2detleiblem5  20922  m2detleiblem3  20926  m2detleiblem4  20927  m2detleib  20928  indistopon  21297  indiscld  21387  xpstopnlem1  22105  xpstopnlem2  22107  xpsdsval  22678  ehl2eudis  23712  i1f1lem  23977  i1f1  23978  dvnfre  24236  c1lip2  24282  aannenlem2  24605  cxplogb  25049  ppiublem2  25465  lgsdir2lem3  25589  eengbas  26454  ebtwntg  26455  structvtxval  26493  usgr2trlncl  27227  umgrwwlks2on  27422  wlk2v2e  27622  eulerpathpr  27705  s2rn  30296  trsp2cyc  30408  cyc3fv1  30412  cnmsgn0g  30421  psgnid  30423  prsiga  31003  coinflippvt  31355  subfacp1lem3  32039  kur14lem7  32069  ex-sategoelel12  32284  noxp1o  32781  noextendlt  32787  nosepdmlem  32798  nolt02o  32810  nosupbnd1lem5  32823  nosupbnd2lem1  32826  noetalem1  32828  onint1  33408  poimirlem22  34466  pw2f1ocnv  39140  fvrcllb0d  39544  fvrcllb0da  39545  corclrcl  39558  relexp0idm  39566  corcltrcl  39590  mnuprdlem1  40126  mnuprdlem3  40128  mnurndlem1  40135  refsum2cnlem1  40854  limsup10exlem  41616  fourierdlem103  42058  fourierdlem104  42059  prsal  42167  zlmodzxzscm  43905  zlmodzxzldeplem3  44059  rrx2pxel  44201  rrx2linesl  44233  2sphere0  44240