Theorem prid1 4706

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  prid2  4707  prnz  4721  preq12b  4793  unisn2  5247  opi1  5421  opeluu  5423  dmrnssfld  5929  funopg  6532  fprb  7149  fveqf1o  7257  2dom  8977  dif1en  9096  opthreg  9539  djuss  9844  dfac2b  10053  brdom7disj  10453  brdom6disj  10454  reelprrecn  11130  pnfxr  11199  m1expcl2  14047  hash2prb  14434  sadcf  16422  prmreclem2  16888  fnpr2ob  17522  setcepi  18055  setc2obas  18061  setc2ohom  18062  cat1  18064  grpss  18930  efgi0  19695  vrgpf  19743  vrgpinv  19744  frgpuptinv  19746  frgpup2  19751  frgpnabllem1  19848  dmdprdpr  20026  dprdpr  20027  cnmsgnsubg  21557  m2detleiblem5  22590  m2detleiblem3  22594  m2detleiblem4  22595  m2detleib  22596  indistopon  22966  indiscld  23056  xpstopnlem1  23774  xpstopnlem2  23776  xpsdsval  24346  ehl2eudis  25389  i1f1lem  25656  i1f1  25657  dvnfre  25919  c1lip2  25965  aannenlem2  26295  cxplogb  26750  ppiublem2  27166  lgsdir2lem3  27290  noxp1o  27627  noextendlt  27633  nosepdmlem  27647  nolt02o  27659  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfno  27682  noinfbnd1  27693  noinfbnd2lem1  27694  noetasuplem1  27697  eengbas  29050  ebtwntg  29051  structvtxval  29090  usgr2trlncl  29828  usgrwwlks2on  30026  umgrwwlks2on  30027  wlk2v2e  30227  eulerpathpr  30310  s2rnOLD  33004  psgnid  33158  trsp2cyc  33184  cyc3fv1  33198  cnmsgn0g  33207  constr01  33886  constrss  33887  constrconj  33889  constrelextdg2  33891  nn0constr  33905  prsiga  34275  coinflippvt  34629  subfacp1lem3  35364  kur14lem7  35394  ex-sategoelel12  35609  onint1  36631  poimirlem22  37963  pw2f1ocnv  43465  2omomeqom  43731  omcl3g  43762  fvrcllb0d  44120  fvrcllb0da  44121  corclrcl  44134  relexp0idm  44142  corcltrcl  44166  mnuprdlem1  44699  mnuprdlem3  44701  mnurndlem1  44708  nregmodellem  45443  refsum2cnlem1  45468  limsup10exlem  46200  fourierdlem103  46637  fourierdlem104  46638  prsal  46746  usgrgrtrirex  48426  stgr1  48437  stgrnbgr0  48440  grlimgrtrilem1  48477  gpgiedgdmellem  48522  gpgvtx0  48529  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem9  48579  zlmodzxzscm  48833  zlmodzxzldeplem3  48978  2arympt  49125  rrx2pxel  49187  rrx2linesl  49219  2sphere0  49226  setc1onsubc  50077