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

Theorem snnzg 4709
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 4598 . 2 (𝐴𝑉𝐴 ∈ {𝐴})
21ne0d 4300 1 (𝐴𝑉 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  wne 3016  c0 4290  {csn 4566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-dif 3938  df-nul 4291  df-sn 4567
This theorem is referenced by:  snnz  4710  0nelop  5385  frirr  5531  frsn  5638  omsucne  7597  1stconst  7794  2ndconst  7795  fczsupp0  7858  hashge3el3dif  13843  pwsbas  16759  pwsle  16764  trnei  22499  uffix  22528  neiflim  22581  hausflim  22588  flimcf  22589  flimclslem  22591  cnpflf2  22607  cnpflf  22608  fclsfnflim  22634  ustneism  22831  ustuqtop5  22853  neipcfilu  22904  dv11cn  24597  cosnop  30430  noextendseq  33174  scutbdaylt  33276  elpaddat  36939  elpadd2at  36941  mnuprdlem1  40608  snn0d  41349  ovnovollem3  42941
  Copyright terms: Public domain W3C validator