Theorem prid1 4726

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  prid2  4727  prnz  4741  preq12b  4814  unisn2  5267  opi1  5428  opeluu  5430  dmrnssfld  5937  funopg  6550  fprb  7168  fveqf1o  7277  2dom  9001  dif1en  9124  dif1enOLD  9126  opthreg  9571  djuss  9873  dfac2b  10084  brdom7disj  10484  brdom6disj  10485  reelprrecn  11160  pnfxr  11228  m1expcl2  14050  hash2prb  14437  sadcf  16423  prmreclem2  16888  fnpr2ob  17521  setcepi  18050  setc2obas  18056  setc2ohom  18057  cat1  18059  grpss  18886  efgi0  19650  vrgpf  19698  vrgpinv  19699  frgpuptinv  19701  frgpup2  19706  frgpnabllem1  19803  dmdprdpr  19981  dprdpr  19982  cnmsgnsubg  21486  m2detleiblem5  22512  m2detleiblem3  22516  m2detleiblem4  22517  m2detleib  22518  indistopon  22888  indiscld  22978  xpstopnlem1  23696  xpstopnlem2  23698  xpsdsval  24269  ehl2eudis  25322  i1f1lem  25590  i1f1  25591  dvnfre  25856  c1lip2  25903  aannenlem2  26237  cxplogb  26696  ppiublem2  27114  lgsdir2lem3  27238  noxp1o  27575  noextendlt  27581  nosepdmlem  27595  nolt02o  27607  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfno  27630  noinfbnd1  27641  noinfbnd2lem1  27642  noetasuplem1  27645  eengbas  28908  ebtwntg  28909  structvtxval  28948  usgr2trlncl  29690  umgrwwlks2on  29887  wlk2v2e  30086  eulerpathpr  30169  s2rnOLD  32865  psgnid  33054  trsp2cyc  33080  cyc3fv1  33094  cnmsgn0g  33103  constr01  33732  constrss  33733  constrconj  33735  constrelextdg2  33737  nn0constr  33751  prsiga  34121  coinflippvt  34476  subfacp1lem3  35169  kur14lem7  35199  ex-sategoelel12  35414  onint1  36437  poimirlem22  37636  pw2f1ocnv  43026  2omomeqom  43292  omcl3g  43323  fvrcllb0d  43682  fvrcllb0da  43683  corclrcl  43696  relexp0idm  43704  corcltrcl  43728  mnuprdlem1  44261  mnuprdlem3  44263  mnurndlem1  44270  nregmodellem  45006  refsum2cnlem1  45031  limsup10exlem  45770  fourierdlem103  46207  fourierdlem104  46208  prsal  46316  usgrgrtrirex  47949  stgr1  47960  stgrnbgr0  47963  grlimgrtrilem1  47993  gpgiedgdmellem  48037  gpgvtx0  48044  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem9  48093  zlmodzxzscm  48345  zlmodzxzldeplem3  48491  2arympt  48638  rrx2pxel  48700  rrx2linesl  48732  2sphere0  48739  setc1onsubc  49591