Theorem prid1 4787

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  prid2  4788  prnz  4802  preq12b  4875  unisn2  5330  opi1  5488  opeluu  5490  dmrnssfld  5996  funopg  6612  fprb  7231  fveqf1o  7338  2dom  9095  dif1en  9226  dif1enOLD  9228  opthreg  9687  djuss  9989  dfac2b  10200  brdom7disj  10600  brdom6disj  10601  reelprrecn  11276  pnfxr  11344  m1expcl2  14136  hash2prb  14521  sadcf  16499  prmreclem2  16964  fnpr2ob  17618  setcepi  18155  setc2obas  18161  setc2ohom  18162  cat1  18164  grpss  18994  efgi0  19762  vrgpf  19810  vrgpinv  19811  frgpuptinv  19813  frgpup2  19818  frgpnabllem1  19915  dmdprdpr  20093  dprdpr  20094  cnmsgnsubg  21618  m2detleiblem5  22652  m2detleiblem3  22656  m2detleiblem4  22657  m2detleib  22658  indistopon  23029  indiscld  23120  xpstopnlem1  23838  xpstopnlem2  23840  xpsdsval  24412  ehl2eudis  25475  i1f1lem  25743  i1f1  25744  dvnfre  26010  c1lip2  26057  aannenlem2  26389  cxplogb  26847  ppiublem2  27265  lgsdir2lem3  27389  noxp1o  27726  noextendlt  27732  nosepdmlem  27746  nolt02o  27758  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfno  27781  noinfbnd1  27792  noinfbnd2lem1  27793  noetasuplem1  27796  eengbas  29014  ebtwntg  29015  structvtxval  29056  usgr2trlncl  29796  umgrwwlks2on  29990  wlk2v2e  30189  eulerpathpr  30272  s2rnOLD  32910  psgnid  33090  trsp2cyc  33116  cyc3fv1  33130  cnmsgn0g  33139  constr01  33732  constrss  33733  constrconj  33735  constrelextdg2  33737  prsiga  34095  coinflippvt  34449  subfacp1lem3  35150  kur14lem7  35180  ex-sategoelel12  35395  onint1  36415  poimirlem22  37602  pw2f1ocnv  42994  2omomeqom  43265  omcl3g  43296  fvrcllb0d  43655  fvrcllb0da  43656  corclrcl  43669  relexp0idm  43677  corcltrcl  43701  mnuprdlem1  44241  mnuprdlem3  44243  mnurndlem1  44250  refsum2cnlem1  44937  limsup10exlem  45693  fourierdlem103  46130  fourierdlem104  46131  prsal  46239  usgrgrtrirex  47799  grlimgrtrilem1  47818  zlmodzxzscm  48082  zlmodzxzldeplem3  48231  2arympt  48383  rrx2pxel  48445  rrx2linesl  48477  2sphere0  48484