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

Theorem snnzg 4496
Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)
Assertion
Ref Expression
snnzg (𝐴𝑉 → {𝐴} ≠ ∅)

Proof of Theorem snnzg
StepHypRef Expression
1 snidg 4398 . 2 (𝐴𝑉𝐴 ∈ {𝐴})
21ne0d 4122 1 (𝐴𝑉 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  wne 2971  c0 4115  {csn 4368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-v 3387  df-dif 3772  df-nul 4116  df-sn 4369
This theorem is referenced by:  snnz  4497  0nelop  5150  frirr  5289  frsn  5394  1stconst  7502  2ndconst  7503  fczsupp0  7562  hashge3el3dif  13517  pwsbas  16462  pwsle  16467  trnei  22024  uffix  22053  neiflim  22106  hausflim  22113  flimcf  22114  flimclslem  22116  cnpflf2  22132  cnpflf  22133  fclsfnflim  22159  ustneism  22355  ustuqtop5  22377  neipcfilu  22428  dv11cn  24105  noextendseq  32333  scutbdaylt  32435  elpaddat  35825  elpadd2at  35827  snn0d  40017  ovnovollem3  41618
  Copyright terms: Public domain W3C validator