Theorem prid1 4767

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  prid2  4768  prnz  4782  preq12b  4852  unisn2  5313  opi1  5469  opeluu  5471  dmrnssfld  5970  funopg  6583  fprb  7195  fveqf1o  7301  2dom  9030  dif1en  9160  dif1enOLD  9162  opthreg  9613  djuss  9915  dfac2b  10125  brdom7disj  10526  brdom6disj  10527  reelprrecn  11202  pnfxr  11268  m1expcl2  14051  hash2prb  14433  sadcf  16394  prmreclem2  16850  fnpr2ob  17504  setcepi  18038  setc2obas  18044  setc2ohom  18045  cat1  18047  grpss  18840  efgi0  19588  vrgpf  19636  vrgpinv  19637  frgpuptinv  19639  frgpup2  19644  frgpnabllem1  19741  dmdprdpr  19919  dprdpr  19920  cnmsgnsubg  21130  m2detleiblem5  22127  m2detleiblem3  22131  m2detleiblem4  22132  m2detleib  22133  indistopon  22504  indiscld  22595  xpstopnlem1  23313  xpstopnlem2  23315  xpsdsval  23887  ehl2eudis  24939  i1f1lem  25206  i1f1  25207  dvnfre  25469  c1lip2  25515  aannenlem2  25842  cxplogb  26291  ppiublem2  26706  lgsdir2lem3  26830  noxp1o  27166  noextendlt  27172  nosepdmlem  27186  nolt02o  27198  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinfno  27221  noinfbnd1  27232  noinfbnd2lem1  27233  noetasuplem1  27236  eengbas  28239  ebtwntg  28240  structvtxval  28281  usgr2trlncl  29017  umgrwwlks2on  29211  wlk2v2e  29410  eulerpathpr  29493  s2rn  32110  psgnid  32256  trsp2cyc  32282  cyc3fv1  32296  cnmsgn0g  32305  prsiga  33129  coinflippvt  33483  subfacp1lem3  34173  kur14lem7  34203  ex-sategoelel12  34418  onint1  35334  poimirlem22  36510  pw2f1ocnv  41776  2omomeqom  42053  omcl3g  42084  fvrcllb0d  42444  fvrcllb0da  42445  corclrcl  42458  relexp0idm  42466  corcltrcl  42490  mnuprdlem1  43031  mnuprdlem3  43033  mnurndlem1  43040  refsum2cnlem1  43721  limsup10exlem  44488  fourierdlem103  44925  fourierdlem104  44926  prsal  45034  zlmodzxzscm  47033  zlmodzxzldeplem3  47183  2arympt  47335  rrx2pxel  47397  rrx2linesl  47429  2sphere0  47436