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

Theorem snid 4025
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 4024 . 2  |-  ( A  e.  _V  <->  A  e.  { A } )
31, 2mpbi 212 1  |-  A  e. 
{ A }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869   _Vcvv 3082   {csn 3997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-sn 3998
This theorem is referenced by:  ssnid  4026  rabsnt  4075  sneqr  4165  sseliALT  4555  elALT  4662  intid  4677  opthprc  4899  dmsnsnsn  5331  snsn0non  5558  fvrn0  5901  fsn  6074  fsn2  6075  fnsnb  6096  fmptsng  6098  fmptsnd  6099  fvsn  6110  fvsnun1  6112  ovima0  6460  brtpos0  6986  tfrlem11  7112  mapsn  7519  mapsncnv  7524  0elixp  7559  domunsncan  7676  enfixsn  7685  infeq5i  8145  tc2  8229  isfin4-3  8747  fin1a2lem12  8843  dcomex  8879  axdc3lem4  8885  zornn0g  8937  axpowndlem3  9026  canthp1lem2  9080  elreal2  9558  xrinfmss  11597  fseq1p1m1  11870  1exp  12302  wrdexb  12681  0bits  14406  lcmfunsnlem2  14606  0ram  14971  setsid  15157  imasvscafn  15436  imasvscaval  15437  xpsc0  15459  xpsc1  15460  gsumval2  16516  gsumz  16614  psgnsn  17154  psgnprfval2  17157  mat0dimscm  19486  mat0scmat  19555  mvmumamul1  19571  m1detdiag  19614  pmatcoe1fsupp  19717  d0mat2pmat  19754  pmatcollpw3fi1lem1  19802  pmatcollpw3fi1lem2  19803  chpmat0d  19850  dfac14  20625  filcon  20890  uffix  20928  cnextfvval  21072  cnextcn  21074  ust0  21226  bndth  21978  minveclem4a  22364  minveclem4aOLD  22376  dvef  22924  tdeglem2  23002  mdegcl  23010  aalioulem2  23281  cxplogb  23715  xrlimcnp  23886  axlowdimlem8  24971  axlowdimlem11  24974  vdgrf  25618  frgrancvvdeqlem7  25756  frgrancvvdeqlemA  25757  grposn  25935  rngosn  26124  hsn0elch  26893  rabsnel  28131  aciunf1lem  28260  esum2dlem  28915  signstfvn  29460  bnj145OLD  29537  bnj97  29679  bnj553  29711  bnj966  29757  bnj1442  29860  subfacp1lem2a  29905  subfacp1lem5  29909  cvmliftlem4  30013  ghomsn  30308  bj-0eltag  31534  poimirlem3  31901  poimirlem9  31907  poimirlem31  31929  poimirlem32  31930  prdsbnd  32083  heiborlem3  32103  grpokerinj  32141  0idl  32216  0rngo  32218  fvilbdRP  36186  frege54cor1c  36413  binomcxplemnotnn0  36607  snsslVD  37130  snssl  37131  unipwrVD  37133  unipwr  37134  sucidALTVD  37172  sucidALT  37173  sucidVD  37174  unisnALT  37228  0cnf  37618  dvmptfprod  37684  nnfoctbdjlem  38116  isomenndlem  38174  funressnfv  38386  el1fzopredsuc  38478  c0snmhm  39257  lincval0  39552  lcoel0  39565
  Copyright terms: Public domain W3C validator