Theorem prid1 4729

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

Syntax hints:   ∈ wcel 2107  Vcvv 3447  {cpr 4594

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 2703

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 2710  df-cleq 2724  df-clel 2810  df-v 3449  df-un 3919  df-sn 4593  df-pr 4595

This theorem is referenced by:  prid2  4730  prnz  4744  preq12b  4814  unisn2  5275  opi1  5431  opeluu  5433  dmrnssfld  5931  funopg  6541  fprb  7149  fveqf1o  7255  2dom  8982  dif1en  9112  dif1enOLD  9114  opthreg  9564  djuss  9866  dfac2b  10076  brdom7disj  10477  brdom6disj  10478  reelprrecn  11153  pnfxr  11219  m1expcl2  14002  hash2prb  14384  sadcf  16345  prmreclem2  16801  fnpr2ob  17455  setcepi  17989  setc2obas  17995  setc2ohom  17996  cat1  17998  grpss  18783  efgi0  19517  vrgpf  19565  vrgpinv  19566  frgpuptinv  19568  frgpup2  19573  frgpnabllem1  19666  dmdprdpr  19843  dprdpr  19844  cnmsgnsubg  21019  m2detleiblem5  22012  m2detleiblem3  22016  m2detleiblem4  22017  m2detleib  22018  indistopon  22389  indiscld  22480  xpstopnlem1  23198  xpstopnlem2  23200  xpsdsval  23772  ehl2eudis  24824  i1f1lem  25091  i1f1  25092  dvnfre  25354  c1lip2  25400  aannenlem2  25727  cxplogb  26174  ppiublem2  26589  lgsdir2lem3  26713  noxp1o  27049  noextendlt  27055  nosepdmlem  27069  nolt02o  27081  nosupbnd1lem5  27098  nosupbnd2lem1  27101  noinfno  27104  noinfbnd1  27115  noinfbnd2lem1  27116  noetasuplem1  27119  eengbas  27994  ebtwntg  27995  structvtxval  28036  usgr2trlncl  28772  umgrwwlks2on  28966  wlk2v2e  29165  eulerpathpr  29248  s2rn  31871  psgnid  32017  trsp2cyc  32043  cyc3fv1  32057  cnmsgn0g  32066  prsiga  32820  coinflippvt  33174  subfacp1lem3  33864  kur14lem7  33894  ex-sategoelel12  34109  onint1  34998  poimirlem22  36174  pw2f1ocnv  41420  2omomeqom  41697  omcl3g  41728  fvrcllb0d  42069  fvrcllb0da  42070  corclrcl  42083  relexp0idm  42091  corcltrcl  42115  mnuprdlem1  42656  mnuprdlem3  42658  mnurndlem1  42665  refsum2cnlem1  43346  limsup10exlem  44115  fourierdlem103  44552  fourierdlem104  44553  prsal  44661  zlmodzxzscm  46535  zlmodzxzldeplem3  46685  2arympt  46837  rrx2pxel  46899  rrx2linesl  46931  2sphere0  46938