Theorem prid1 4719

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  prid2  4720  prnz  4734  preq12b  4806  unisn2  5257  opi1  5416  opeluu  5418  dmrnssfld  5923  funopg  6526  fprb  7140  fveqf1o  7248  2dom  8967  dif1en  9086  opthreg  9527  djuss  9832  dfac2b  10041  brdom7disj  10441  brdom6disj  10442  reelprrecn  11118  pnfxr  11186  m1expcl2  14008  hash2prb  14395  sadcf  16380  prmreclem2  16845  fnpr2ob  17479  setcepi  18012  setc2obas  18018  setc2ohom  18019  cat1  18021  grpss  18884  efgi0  19649  vrgpf  19697  vrgpinv  19698  frgpuptinv  19700  frgpup2  19705  frgpnabllem1  19802  dmdprdpr  19980  dprdpr  19981  cnmsgnsubg  21532  m2detleiblem5  22569  m2detleiblem3  22573  m2detleiblem4  22574  m2detleib  22575  indistopon  22945  indiscld  23035  xpstopnlem1  23753  xpstopnlem2  23755  xpsdsval  24325  ehl2eudis  25378  i1f1lem  25646  i1f1  25647  dvnfre  25912  c1lip2  25959  aannenlem2  26293  cxplogb  26752  ppiublem2  27170  lgsdir2lem3  27294  noxp1o  27631  noextendlt  27637  nosepdmlem  27651  nolt02o  27663  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfno  27686  noinfbnd1  27697  noinfbnd2lem1  27698  noetasuplem1  27701  eengbas  29054  ebtwntg  29055  structvtxval  29094  usgr2trlncl  29833  usgrwwlks2on  30031  umgrwwlks2on  30032  wlk2v2e  30232  eulerpathpr  30315  s2rnOLD  33026  psgnid  33179  trsp2cyc  33205  cyc3fv1  33219  cnmsgn0g  33228  constr01  33899  constrss  33900  constrconj  33902  constrelextdg2  33904  nn0constr  33918  prsiga  34288  coinflippvt  34642  subfacp1lem3  35376  kur14lem7  35406  ex-sategoelel12  35621  onint1  36643  poimirlem22  37843  pw2f1ocnv  43279  2omomeqom  43545  omcl3g  43576  fvrcllb0d  43934  fvrcllb0da  43935  corclrcl  43948  relexp0idm  43956  corcltrcl  43980  mnuprdlem1  44513  mnuprdlem3  44515  mnurndlem1  44522  nregmodellem  45257  refsum2cnlem1  45282  limsup10exlem  46016  fourierdlem103  46453  fourierdlem104  46454  prsal  46562  usgrgrtrirex  48196  stgr1  48207  stgrnbgr0  48210  grlimgrtrilem1  48247  gpgiedgdmellem  48292  gpgvtx0  48299  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem9  48349  zlmodzxzscm  48603  zlmodzxzldeplem3  48748  2arympt  48895  rrx2pxel  48957  rrx2linesl  48989  2sphere0  48996  setc1onsubc  49847