Theorem prid1 4724

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

Syntax hints:   ∈ wcel 2145  Vcvv 3457  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  prid2  4725  prnz  4739  preq12b  4810  unisn2  5266  opi1  5440  opeluu  5442  dmrnssfld  5954  funopg  6559  fprb  7182  fveqf1o  7290  2dom  9015  dif1en  9134  opthreg  9575  djuss  9894  dfac2b  10102  brdom7disj  10503  brdom6disj  10504  reelprrecn  11180  0elpr01  11189  pnfxr  11251  m1expcl2  14109  hash2prb  14497  sadcf  16499  prmreclem2  16965  fnpr2ob  17600  setcepi  18133  setc2obas  18139  setc2ohom  18140  cat1  18142  grpss  19009  efgi0  19778  vrgpf  19826  vrgpinv  19827  frgpuptinv  19829  frgpup2  19834  frgpnabllem1  19931  dmdprdpr  20109  dprdpr  20110  cnmsgnsubg  21684  m2detleiblem5  22739  m2detleiblem3  22743  m2detleiblem4  22744  m2detleib  22745  indistopon  23115  indiscld  23205  xpstopnlem1  23923  xpstopnlem2  23925  xpsdsval  24495  ehl2eudis  25538  i1f1lem  25805  i1f1  25806  dvnfre  26068  c1lip2  26114  aannenlem2  26447  cxplogb  26905  ppiublem2  27321  lgsdir2lem3  27445  noxp1o  27781  noextendlt  27787  nosepdmlem  27801  nolt02o  27813  nosupbnd1lem5  27830  nosupbnd2lem1  27833  noinfno  27836  noinfbnd1  27847  noinfbnd2lem1  27848  noetasuplem1  27851  eengbas  29236  ebtwntg  29237  structvtxval  29276  usgr2trlncl  30014  usgrwwlks2on  30212  umgrwwlks2on  30213  wlk2v2e  30413  eulerpathpr  30496  s2rnOLD  33172  psgnid  33325  trsp2cyc  33351  cyc3fv1  33365  cnmsgn0g  33374  constr01  34044  constrss  34045  constrelextdg2  34049  nn0constr  34063  prsiga  34433  coinflippvt  34787  subfacp1lem3  35540  kur14lem7  35570  ex-sategoelel12  35785  onint1  36817  poimirlem22  38148  pw2f1ocnv  43621  2omomeqom  43887  omcl3g  43918  fvrcllb0d  44276  fvrcllb0da  44277  corclrcl  44290  relexp0idm  44298  corcltrcl  44322  mnuprdlem1  44841  mnuprdlem3  44843  mnurndlem1  44850  nregmodellem  45584  refsum2cnlem1  45616  limsup10exlem  46345  fourierdlem103  46782  fourierdlem104  46783  prsal  46891  usgrgrtrirex  48571  stgr1  48582  stgrnbgr0  48585  grlimgrtrilem1  48622  gpgiedgdmellem  48667  gpgvtx0  48674  gpgprismgr4cycllem3  48718  gpgprismgr4cycllem9  48724  zlmodzxzscm  48989  zlmodzxzldeplem3  49134  2arympt  49281  rrx2pxel  49343  rrx2linesl  49375  2sphere0  49382  setc1onsubc  50232