Theorem prid1 4768

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

Syntax hints:   ∈ wcel 2098  Vcvv 3461  {cpr 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-sn 4631  df-pr 4633

This theorem is referenced by:  prid2  4769  prnz  4783  preq12b  4853  unisn2  5313  opi1  5470  opeluu  5472  dmrnssfld  5973  funopg  6588  fprb  7206  fveqf1o  7311  2dom  9056  dif1en  9188  dif1enOLD  9190  opthreg  9648  djuss  9950  dfac2b  10160  brdom7disj  10561  brdom6disj  10562  reelprrecn  11237  pnfxr  11305  m1expcl2  14091  hash2prb  14474  sadcf  16436  prmreclem2  16894  fnpr2ob  17548  setcepi  18085  setc2obas  18091  setc2ohom  18092  cat1  18094  grpss  18924  efgi0  19692  vrgpf  19740  vrgpinv  19741  frgpuptinv  19743  frgpup2  19748  frgpnabllem1  19845  dmdprdpr  20023  dprdpr  20024  cnmsgnsubg  21531  m2detleiblem5  22576  m2detleiblem3  22580  m2detleiblem4  22581  m2detleib  22582  indistopon  22953  indiscld  23044  xpstopnlem1  23762  xpstopnlem2  23764  xpsdsval  24336  ehl2eudis  25399  i1f1lem  25667  i1f1  25668  dvnfre  25933  c1lip2  25980  aannenlem2  26314  cxplogb  26768  ppiublem2  27186  lgsdir2lem3  27310  noxp1o  27647  noextendlt  27653  nosepdmlem  27667  nolt02o  27679  nosupbnd1lem5  27696  nosupbnd2lem1  27699  noinfno  27702  noinfbnd1  27713  noinfbnd2lem1  27714  noetasuplem1  27717  eengbas  28869  ebtwntg  28870  structvtxval  28911  usgr2trlncl  29651  umgrwwlks2on  29845  wlk2v2e  30044  eulerpathpr  30127  s2rn  32759  psgnid  32915  trsp2cyc  32941  cyc3fv1  32955  cnmsgn0g  32964  prsiga  33883  coinflippvt  34237  subfacp1lem3  34925  kur14lem7  34955  ex-sategoelel12  35170  onint1  36066  poimirlem22  37248  pw2f1ocnv  42602  2omomeqom  42876  omcl3g  42907  fvrcllb0d  43267  fvrcllb0da  43268  corclrcl  43281  relexp0idm  43289  corcltrcl  43313  mnuprdlem1  43853  mnuprdlem3  43855  mnurndlem1  43862  refsum2cnlem1  44543  limsup10exlem  45300  fourierdlem103  45737  fourierdlem104  45738  prsal  45846  zlmodzxzscm  47609  zlmodzxzldeplem3  47758  2arympt  47910  rrx2pxel  47972  rrx2linesl  48004  2sphere0  48011