Theorem prid1 4723

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  prid2  4724  prnz  4738  preq12b  4810  unisn2  5266  opi1  5437  opeluu  5439  dmrnssfld  5956  funopg  6566  fprb  7191  fveqf1o  7302  2dom  9042  dif1en  9161  opthreg  9603  djuss  9982  dfac2b  10190  brdom7disj  10591  brdom6disj  10592  reelprrecn  11273  0elpr01  11282  pnfxr  11344  m1expcl2  14208  hash2prb  14597  sadcf  16603  fnpr2ob  17710  setcepi  18243  setc2obas  18249  setc2ohom  18250  cat1  18252  degenmgm  19117  degenmgm2  19120  grpss  19145  efgi0  19914  vrgpf  19962  vrgpinv  19963  frgpuptinv  19965  frgpup2  19970  frgpnabllem1  20067  dmdprdpr  20245  dprdpr  20246  cnmsgnsubg  21863  m2detleiblem5  22920  m2detleiblem3  22924  m2detleiblem4  22925  m2detleib  22926  indistopon  23299  indiscld  23389  xpstopnlem1  24108  xpstopnlem2  24110  xpsdsval  24680  ehl2eudis  25723  dvnfre  26252  c1lip2  26298  aannenlem2  26638  ppiublem2  27512  lgsdir2lem3  27636  noxp1o  28002  noextendlt  28008  nosepdmlem  28022  nolt02o  28034  nosupbnd1lem5  28051  nosupbnd2lem1  28054  noinfno  28057  noinfbnd1  28068  noinfbnd2lem1  28069  noetasuplem1  28072  eengbas  29541  ebtwntg  29542  structvtxval  29581  wlk2v2e  30740  eulerpathpr  30823  psgnid  33640  trsp2cyc  33666  cnmsgn0g  33689  prsiga  34745  coinflippvt  35100  subfacp1lem3  35916  kur14lem7  35946  ex-sategoelel12  36161  onint1  37207  poimirlem22  38528  pw2f1ocnv  43997  2omomeqom  44263  omcl3g  44294  relexp0idm  44674  corcltrcl  44698  mnuprdlem1  45215  mnuprdlem3  45217  mnurndlem1  45224  nregmodellem  45958  refsum2cnlem1  45997  fourierdlem103  47163  fourierdlem104  47164  prsal  47272  usgrgrtrirex  48992  stgrnbgr0  49006  grlimgrtrilem1  49043  zlmodzxzldeplem3  49558  rrx2pxel  49767  rrx2linesl  49799  2sphere0  49806  setc1onsubc  50654