MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snid Structured version   Unicode version

Theorem snid 3972
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
snid.1  |-  A  e. 
_V
Assertion
Ref Expression
snid  |-  A  e. 
{ A }

Proof of Theorem snid
StepHypRef Expression
1 snid.1 . 2  |-  A  e. 
_V
2 snidb 3971 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 208 1  |-  A  e. 
{ A }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   _Vcvv 3034   {csn 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-sn 3945
This theorem is referenced by:  ssnid  3973  rabsnt  4021  sneqr  4111  sseliALT  4498  elALT  4605  intid  4620  snsn0non  4910  opthprc  4961  dmsnsnsn  5394  fvrn0  5796  fsn  5971  fsn2  5973  fnsnb  5992  fmptsng  5994  fmptsnd  5995  fvsn  6006  fvsnun1  6008  ovima0  6353  brtpos0  6880  tfrlem11  6975  mapsn  7379  mapsncnv  7384  0elixp  7419  domunsncan  7536  enfixsn  7545  infeq5i  7967  tc2  8086  isfin4-3  8608  fin1a2lem12  8704  dcomex  8740  axdc3lem4  8746  zornn0g  8798  axpowndlem3  8887  canthp1lem2  8942  elreal2  9420  xrinfmss  11422  fseq1p1m1  11674  1exp  12098  wrdexb  12465  0bits  14091  0ram  14540  setsid  14677  imasvscafn  14944  imasvscaval  14945  xpsc0  14967  xpsc1  14968  gsumval2  16024  gsumz  16122  psgnsn  16662  psgnprfval2  16665  mat0dimscm  19056  mat0scmat  19125  mvmumamul1  19141  m1detdiag  19184  pmatcoe1fsupp  19287  d0mat2pmat  19324  pmatcollpw3fi1lem1  19372  pmatcollpw3fi1lem2  19373  chpmat0d  19420  dfac14  20204  filcon  20469  uffix  20507  cnextfvval  20650  cnextcn  20652  ust0  20807  bndth  21543  minveclem4a  21930  dvef  22466  tdeglem2  22544  mdegcl  22554  aalioulem2  22814  cxplogb  23244  xrlimcnp  23415  axlowdimlem8  24373  axlowdimlem11  24376  vdgrf  25019  frgrancvvdeqlem7  25157  frgrancvvdeqlemA  25158  grposn  25334  rngosn  25523  hsn0elch  26283  rabsnel  27520  aciunf1lem  27648  esum2dlem  28240  signstfvn  28709  subfacp1lem2a  28813  subfacp1lem5  28817  cvmliftlem4  28922  ghomsn  29217  prdsbnd  30455  heiborlem3  30475  grpokerinj  30513  0idl  30588  0rngo  30590  binomcxplemnotnn0  31429  0cnf  31845  dvmptfprod  31908  funressnfv  32379  c0snmhm  32921  lincval0  33216  lcoel0  33229  snsslVD  33975  snssl  33976  unipwrVD  33978  unipwr  33979  sucidALTVD  34017  sucidALT  34018  sucidVD  34019  unisnALT  34073  bnj145OLD  34129  bnj97  34271  bnj553  34303  bnj966  34349  bnj1442  34452  bj-0eltag  34884  frege54cor1c  38414
  Copyright terms: Public domain W3C validator