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

Theorem snnzg 3864
Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
Assertion
Ref Expression
snnzg  |-  ( A  e.  V  ->  { A }  =/=  (/) )

Proof of Theorem snnzg
StepHypRef Expression
1 snidg 3782 . 2  |-  ( A  e.  V  ->  A  e.  { A } )
2 ne0i 3577 . 2  |-  ( A  e.  { A }  ->  { A }  =/=  (/) )
31, 2syl 16 1  |-  ( A  e.  V  ->  { A }  =/=  (/) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717    =/= wne 2550   (/)c0 3571   {csn 3757
This theorem is referenced by:  snnz  3865  0nelop  4387  frirr  4500  frsn  4888  xpimasn  5256  1stconst  6374  2ndconst  6375  pwsbas  13636  pwsle  13641  trnei  17845  uffix  17874  neiflim  17927  hausflim  17934  flimcf  17935  flimclslem  17937  cnpflf2  17953  cnpflf  17954  fclsfnflim  17980  ustneism  18174  ustuqtop5  18196  neipcfilu  18247  dv11cn  19752  usgra1v  21275  elpaddat  29918  elpadd2at  29920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-v 2901  df-dif 3266  df-nul 3572  df-sn 3763
  Copyright terms: Public domain W3C validator