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

Theorem snssg 4163
Description: The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
Assertion
Ref Expression
snssg

Proof of Theorem snssg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eleq1 2529 . 2
2 sneq 4039 . . 3
32sseq1d 3530 . 2
4 vex 3112 . . 3
54snss 4154 . 2
61, 3, 5vtoclbg 3168 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  C_wss 3475  {csn 4029
This theorem is referenced by:  tppreqb  4171  snssi  4174  snssd  4175  prssg  4185  fvimacnvALT  6006  fr3nr  6615  vdwapid1  14493  acsfn  15056  cycsubg2  16238  cycsubg2cl  16239  pgpfac1lem1  17125  pgpfac1lem3a  17127  pgpfac1lem3  17128  pgpfac1lem5  17130  pgpfaclem2  17133  lspsnid  17639  lidldvgen  17903  isneip  19606  elnei  19612  iscnp4  19764  cnpnei  19765  nlly2i  19977  1stckgenlem  20054  flimopn  20476  flimclslem  20485  fclsneii  20518  fcfnei  20536  limcvallem  22275  ellimc2  22281  limcflf  22285  limccnp  22295  limccnp2  22296  limcco  22297  lhop2  22416  plyrem  22701  isppw  23388  h1did  26469  erdszelem8  28642  neibastop2  30179  prnc  30464  proot1mul  31156  islptre  31625
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-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489  df-sn 4030
  Copyright terms: Public domain W3C validator