Theorem prid1 4762

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  {cpr 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  prid2  4763  prnz  4777  preq12b  4850  unisn2  5312  opi1  5473  opeluu  5475  dmrnssfld  5984  funopg  6600  fprb  7214  fveqf1o  7322  2dom  9070  dif1en  9200  dif1enOLD  9202  opthreg  9658  djuss  9960  dfac2b  10171  brdom7disj  10571  brdom6disj  10572  reelprrecn  11247  pnfxr  11315  m1expcl2  14126  hash2prb  14511  sadcf  16490  prmreclem2  16955  fnpr2ob  17603  setcepi  18133  setc2obas  18139  setc2ohom  18140  cat1  18142  grpss  18972  efgi0  19738  vrgpf  19786  vrgpinv  19787  frgpuptinv  19789  frgpup2  19794  frgpnabllem1  19891  dmdprdpr  20069  dprdpr  20070  cnmsgnsubg  21595  m2detleiblem5  22631  m2detleiblem3  22635  m2detleiblem4  22636  m2detleib  22637  indistopon  23008  indiscld  23099  xpstopnlem1  23817  xpstopnlem2  23819  xpsdsval  24391  ehl2eudis  25456  i1f1lem  25724  i1f1  25725  dvnfre  25990  c1lip2  26037  aannenlem2  26371  cxplogb  26829  ppiublem2  27247  lgsdir2lem3  27371  noxp1o  27708  noextendlt  27714  nosepdmlem  27728  nolt02o  27740  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfno  27763  noinfbnd1  27774  noinfbnd2lem1  27775  noetasuplem1  27778  eengbas  28996  ebtwntg  28997  structvtxval  29038  usgr2trlncl  29780  umgrwwlks2on  29977  wlk2v2e  30176  eulerpathpr  30259  s2rnOLD  32928  psgnid  33117  trsp2cyc  33143  cyc3fv1  33157  cnmsgn0g  33166  constr01  33783  constrss  33784  constrconj  33786  constrelextdg2  33788  prsiga  34132  coinflippvt  34487  subfacp1lem3  35187  kur14lem7  35217  ex-sategoelel12  35432  onint1  36450  poimirlem22  37649  pw2f1ocnv  43049  2omomeqom  43316  omcl3g  43347  fvrcllb0d  43706  fvrcllb0da  43707  corclrcl  43720  relexp0idm  43728  corcltrcl  43752  mnuprdlem1  44291  mnuprdlem3  44293  mnurndlem1  44300  refsum2cnlem1  45042  limsup10exlem  45787  fourierdlem103  46224  fourierdlem104  46225  prsal  46333  usgrgrtrirex  47917  stgr1  47928  stgrnbgr0  47931  grlimgrtrilem1  47961  gpgedgel  48007  gpgvtx0  48008  zlmodzxzscm  48273  zlmodzxzldeplem3  48419  2arympt  48570  rrx2pxel  48632  rrx2linesl  48664  2sphere0  48671