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

Theorem snid 4042
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 4041 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 208 1  |-  A  e. 
{ A }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   _Vcvv 3095   {csn 4014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-sn 4015
This theorem is referenced by:  ssnid  4043  rabsnt  4092  sneqr  4182  sseliALT  4568  reusv6OLD  4648  elALT  4680  intid  4695  snsn0non  4986  opthprc  5037  dmsnsnsn  5476  fvrn0  5878  fsn  6054  fsn2  6056  fnsnb  6075  fmptsng  6077  fmptsnd  6078  fvsn  6089  fvsnun1  6091  ovima0  6439  brtpos0  6964  tfrlem11  7059  mapsn  7462  mapsncnv  7467  0elixp  7502  domunsncan  7619  enfixsn  7628  infeq5i  8056  tc2  8176  isfin4-3  8698  fin1a2lem12  8794  dcomex  8830  axdc3lem4  8836  zornn0g  8888  axpowndlem3  8978  axpowndlem3OLD  8979  canthp1lem2  9034  elreal2  9512  xrinfmss  11510  fseq1p1m1  11761  1exp  12174  wrdexb  12537  0bits  13966  0ram  14415  setsid  14550  imasvscafn  14811  imasvscaval  14812  xpsc0  14834  xpsc1  14835  gsumval2  15781  gsumz  15879  psgnsn  16419  psgnprfval2  16422  mat0dimscm  18844  mat0scmat  18913  mvmumamul1  18929  m1detdiag  18972  pmatcoe1fsupp  19075  d0mat2pmat  19112  pmatcollpw3fi1lem1  19160  pmatcollpw3fi1lem2  19161  chpmat0d  19208  dfac14  19992  filcon  20257  uffix  20295  cnextfvval  20438  cnextcn  20440  ust0  20595  bndth  21331  minveclem4a  21718  dvef  22254  tdeglem2  22332  mdegcl  22342  aalioulem2  22601  xrlimcnp  23170  axlowdimlem8  24124  axlowdimlem11  24127  vdgrf  24770  frgrancvvdeqlem7  24908  frgrancvvdeqlemA  24909  grposn  25089  rngosn  25278  hsn0elch  26038  rabsnel  27274  signstfvn  28399  subfacp1lem2a  28497  subfacp1lem5  28501  cvmliftlem4  28606  ghomsn  28901  prdsbnd  30264  heiborlem3  30284  grpokerinj  30322  0idl  30397  0rngo  30399  0cnf  31586  funressnfv  32051  lincval0  32751  lcoel0  32764  snsslVD  33362  snssl  33363  unipwrVD  33365  unipwr  33366  sucidALTVD  33403  sucidALT  33404  sucidVD  33405  unisnALT  33459  bnj145OLD  33515  bnj97  33657  bnj553  33689  bnj966  33735  bnj1442  33838  bj-0eltag  34284  frege54cor1c  37611
  Copyright terms: Public domain W3C validator