MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prid1 Structured version   Visualization version   GIF version

Theorem prid1 4721
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
StepHypRef Expression
1 prid1.1 . 2 𝐴 ∈ V
2 prid1g 4719 . 2 (𝐴 ∈ V → 𝐴 ∈ {𝐴, 𝐵})
31, 2ax-mp 5 1 𝐴 ∈ {𝐴, 𝐵}
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  Vcvv 3443  {cpr 4586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-un 3913  df-sn 4585  df-pr 4587
This theorem is referenced by:  prid2  4722  prnz  4736  preq12b  4806  unisn2  5267  opi1  5423  opeluu  5425  dmrnssfld  5923  funopg  6532  fprb  7139  fveqf1o  7245  2dom  8932  dif1en  9062  dif1enOLD  9064  opthreg  9512  djuss  9814  dfac2b  10024  brdom7disj  10425  brdom6disj  10426  reelprrecn  11101  pnfxr  11167  m1expcl2  13945  hash2prb  14324  sadcf  16292  prmreclem2  16748  fnpr2ob  17399  setcepi  17933  setc2obas  17939  setc2ohom  17940  cat1  17942  grpss  18727  efgi0  19460  vrgpf  19508  vrgpinv  19509  frgpuptinv  19511  frgpup2  19516  frgpnabllem1  19609  dmdprdpr  19786  dprdpr  19787  cnmsgnsubg  20933  m2detleiblem5  21925  m2detleiblem3  21929  m2detleiblem4  21930  m2detleib  21931  indistopon  22302  indiscld  22393  xpstopnlem1  23111  xpstopnlem2  23113  xpsdsval  23685  ehl2eudis  24737  i1f1lem  25004  i1f1  25005  dvnfre  25267  c1lip2  25313  aannenlem2  25640  cxplogb  26087  ppiublem2  26502  lgsdir2lem3  26626  noxp1o  26962  noextendlt  26968  nosepdmlem  26982  nolt02o  26994  nosupbnd1lem5  27011  nosupbnd2lem1  27014  noinfno  27017  noinfbnd1  27028  noinfbnd2lem1  27029  noetasuplem1  27032  eengbas  27758  ebtwntg  27759  structvtxval  27800  usgr2trlncl  28536  umgrwwlks2on  28730  wlk2v2e  28929  eulerpathpr  29012  s2rn  31624  psgnid  31770  trsp2cyc  31796  cyc3fv1  31810  cnmsgn0g  31819  prsiga  32533  coinflippvt  32887  subfacp1lem3  33579  kur14lem7  33609  ex-sategoelel12  33824  onint1  34852  poimirlem22  36031  pw2f1ocnv  41263  2omomeqom  41538  omcl3g  41567  fvrcllb0d  41869  fvrcllb0da  41870  corclrcl  41883  relexp0idm  41891  corcltrcl  41915  mnuprdlem1  42456  mnuprdlem3  42458  mnurndlem1  42465  refsum2cnlem1  43146  limsup10exlem  43907  fourierdlem103  44344  fourierdlem104  44345  prsal  44453  zlmodzxzscm  46327  zlmodzxzldeplem3  46477  2arympt  46629  rrx2pxel  46691  rrx2linesl  46723  2sphere0  46730
  Copyright terms: Public domain W3C validator