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

Theorem snid 4048
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 4047 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 208 1  |-  A  e. 
{ A }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   _Vcvv 3106   {csn 4020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-sn 4021
This theorem is referenced by:  ssnid  4049  rabsnt  4097  sneqr  4187  sseliALT  4571  reusv6OLD  4651  elALT  4683  intid  4698  snsn0non  4989  opthprc  5039  dmsnsnsn  5477  fvrn0  5879  fsn  6050  fsn2  6052  fnsnb  6071  fmptsng  6073  fmptsnd  6074  fvsn  6085  fvsnun1  6087  ovima0  6429  brtpos0  6952  tfrlem11  7047  mapsn  7450  mapsncnv  7455  0elixp  7490  domunsncan  7607  enfixsn  7616  findcard2d  7751  infeq5i  8042  tc2  8162  isfin4-3  8684  fin1a2lem12  8780  dcomex  8816  axdc3lem4  8822  zornn0g  8874  axpowndlem3  8964  axpowndlem3OLD  8965  canthp1lem2  9020  elreal2  9498  xrinfmss  11490  fseq1p1m1  11741  1exp  12150  wrdexb  12511  0bits  13937  0ram  14386  setsid  14520  imasvscafn  14781  imasvscaval  14782  xpsc0  14804  xpsc1  14805  gsumz  15817  gsumval2  15819  psgnsn  16334  psgnprfval2  16337  mat0dimscm  18731  mat0scmat  18800  mvmumamul1  18816  m1detdiag  18859  maducoeval2  18902  pmatcoe1fsupp  18962  d0mat2pmat  18999  pmatcollpw3fi1lem1  19047  pmatcollpw3fi1lem2  19048  chpmat0d  19095  dfac14  19847  filcon  20112  uffix  20150  cnextfvval  20293  cnextcn  20295  ust0  20450  bndth  21186  minveclem4a  21573  dvef  22109  tdeglem2  22187  mdegcl  22197  aalioulem2  22456  xrlimcnp  23019  axlowdimlem8  23921  axlowdimlem11  23924  vdgrf  24560  frgrancvvdeqlem7  24699  frgrancvvdeqlemA  24700  grposn  24879  rngosn  25068  hsn0elch  25828  rabsnel  27064  signstfvn  28152  subfacp1lem2a  28250  subfacp1lem5  28254  cvmliftlem4  28359  ghomsn  28489  prdsbnd  29879  heiborlem3  29899  grpokerinj  29937  0idl  30012  0rngo  30014  0cnf  31170  funressnfv  31635  lincval0  31964  lcoel0  31977  snsslVD  32584  snssl  32585  unipwrVD  32587  unipwr  32588  sucidALTVD  32625  sucidALT  32626  sucidVD  32627  unisnALT  32681  bnj145OLD  32737  bnj97  32878  bnj553  32910  bnj966  32956  bnj1442  33059  bj-0eltag  33492  frege54cor1c  36782
  Copyright terms: Public domain W3C validator