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

Theorem snid 4057
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
Assertion
Ref Expression
snid

Proof of Theorem snid
StepHypRef Expression
1 snid.1 . 2
2 snidb 4056 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109  {csn 4029
This theorem is referenced by:  ssnid  4058  rabsnt  4107  sneqr  4197  sseliALT  4583  reusv6OLD  4663  elALT  4695  intid  4710  snsn0non  5001  opthprc  5052  dmsnsnsn  5491  fvrn0  5893  fsn  6069  fsn2  6071  fnsnb  6090  fmptsng  6092  fmptsnd  6093  fvsn  6104  fvsnun1  6106  ovima0  6454  brtpos0  6981  tfrlem11  7076  mapsn  7480  mapsncnv  7485  0elixp  7520  domunsncan  7637  enfixsn  7646  infeq5i  8074  tc2  8194  isfin4-3  8716  fin1a2lem12  8812  dcomex  8848  axdc3lem4  8854  zornn0g  8906  axpowndlem3  8996  axpowndlem3OLD  8997  canthp1lem2  9052  elreal2  9530  xrinfmss  11530  fseq1p1m1  11781  1exp  12195  wrdexb  12558  0bits  14089  0ram  14538  setsid  14673  imasvscafn  14934  imasvscaval  14935  xpsc0  14957  xpsc1  14958  gsumval2  15907  gsumz  16005  psgnsn  16545  psgnprfval2  16548  mat0dimscm  18971  mat0scmat  19040  mvmumamul1  19056  m1detdiag  19099  pmatcoe1fsupp  19202  d0mat2pmat  19239  pmatcollpw3fi1lem1  19287  pmatcollpw3fi1lem2  19288  chpmat0d  19335  dfac14  20119  filcon  20384  uffix  20422  cnextfvval  20565  cnextcn  20567  ust0  20722  bndth  21458  minveclem4a  21845  dvef  22381  tdeglem2  22459  mdegcl  22469  aalioulem2  22729  xrlimcnp  23298  axlowdimlem8  24252  axlowdimlem11  24255  vdgrf  24898  frgrancvvdeqlem7  25036  frgrancvvdeqlemA  25037  grposn  25217  rngosn  25406  hsn0elch  26166  rabsnel  27402  signstfvn  28526  subfacp1lem2a  28624  subfacp1lem5  28628  cvmliftlem4  28733  ghomsn  29028  prdsbnd  30289  heiborlem3  30309  grpokerinj  30347  0idl  30422  0rngo  30424  binomcxplemnotnn0  31261  0cnf  31679  dvmptfprod  31742  funressnfv  32213  c0snmhm  32721  lincval0  33016  lcoel0  33029  snsslVD  33629  snssl  33630  unipwrVD  33632  unipwr  33633  sucidALTVD  33670  sucidALT  33671  sucidVD  33672  unisnALT  33726  bnj145OLD  33782  bnj97  33924  bnj553  33956  bnj966  34002  bnj1442  34105  bj-0eltag  34536  frege54cor1c  37942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sn 4030
  Copyright terms: Public domain W3C validator