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

Theorem snnzg 4710
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 4595 . 2 (𝐴𝑉𝐴 ∈ {𝐴})
21ne0d 4269 1 (𝐴𝑉 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wne 2943  c0 4256  {csn 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-dif 3890  df-nul 4257  df-sn 4562
This theorem is referenced by:  snn0d  4711  snnz  4712  frirr  5566  frsn  5674  omsucne  7731  1stconst  7940  2ndconst  7941  fczsupp0  8009  hashge3el3dif  14200  pwsbas  17198  pwsle  17203  trnei  23043  uffix  23072  neiflim  23125  flimclslem  23135  fclsfnflim  23178  ustneism  23375  ustuqtop5  23397  dv11cn  25165  snsssng  30860  cosnop  31028  noextendseq  33870  scutbdaylt  34012  lltropt  34056  elpadd2at  37820
  Copyright terms: Public domain W3C validator