Theorem prid1 4766

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477  {cpr 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-sn 4631  df-pr 4633

This theorem is referenced by:  prid2  4767  prnz  4781  preq12b  4854  unisn2  5317  opi1  5478  opeluu  5480  dmrnssfld  5986  funopg  6601  fprb  7213  fveqf1o  7321  2dom  9068  dif1en  9198  dif1enOLD  9200  opthreg  9655  djuss  9957  dfac2b  10168  brdom7disj  10568  brdom6disj  10569  reelprrecn  11244  pnfxr  11312  m1expcl2  14122  hash2prb  14507  sadcf  16486  prmreclem2  16950  fnpr2ob  17604  setcepi  18141  setc2obas  18147  setc2ohom  18148  cat1  18150  grpss  18984  efgi0  19752  vrgpf  19800  vrgpinv  19801  frgpuptinv  19803  frgpup2  19808  frgpnabllem1  19905  dmdprdpr  20083  dprdpr  20084  cnmsgnsubg  21612  m2detleiblem5  22646  m2detleiblem3  22650  m2detleiblem4  22651  m2detleib  22652  indistopon  23023  indiscld  23114  xpstopnlem1  23832  xpstopnlem2  23834  xpsdsval  24406  ehl2eudis  25469  i1f1lem  25737  i1f1  25738  dvnfre  26004  c1lip2  26051  aannenlem2  26385  cxplogb  26843  ppiublem2  27261  lgsdir2lem3  27385  noxp1o  27722  noextendlt  27728  nosepdmlem  27742  nolt02o  27754  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinfno  27777  noinfbnd1  27788  noinfbnd2lem1  27789  noetasuplem1  27792  eengbas  29010  ebtwntg  29011  structvtxval  29052  usgr2trlncl  29792  umgrwwlks2on  29986  wlk2v2e  30185  eulerpathpr  30268  s2rnOLD  32912  psgnid  33099  trsp2cyc  33125  cyc3fv1  33139  cnmsgn0g  33148  constr01  33746  constrss  33747  constrconj  33749  constrelextdg2  33751  prsiga  34111  coinflippvt  34465  subfacp1lem3  35166  kur14lem7  35196  ex-sategoelel12  35411  onint1  36431  poimirlem22  37628  pw2f1ocnv  43025  2omomeqom  43292  omcl3g  43323  fvrcllb0d  43682  fvrcllb0da  43683  corclrcl  43696  relexp0idm  43704  corcltrcl  43728  mnuprdlem1  44267  mnuprdlem3  44269  mnurndlem1  44276  refsum2cnlem1  44974  limsup10exlem  45727  fourierdlem103  46164  fourierdlem104  46165  prsal  46273  usgrgrtrirex  47852  stgr1  47863  stgrnbgr0  47866  grlimgrtrilem1  47896  gpgedgel  47942  gpgvtx0  47943  zlmodzxzscm  48201  zlmodzxzldeplem3  48347  2arympt  48498  rrx2pxel  48560  rrx2linesl  48592  2sphere0  48599