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

Theorem snnzg 4339
 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 4239 . 2 (𝐴𝑉𝐴 ∈ {𝐴})
2 ne0i 3954 . 2 (𝐴 ∈ {𝐴} → {𝐴} ≠ ∅)
31, 2syl 17 1 (𝐴𝑉 → {𝐴} ≠ ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2030   ≠ wne 2823  ∅c0 3948  {csn 4210 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-nul 3949  df-sn 4211 This theorem is referenced by:  snnz  4340  0nelop  4989  frirr  5120  frsn  5223  1stconst  7310  2ndconst  7311  fczsupp0  7369  hashge3el3dif  13306  pwsbas  16194  pwsle  16199  trnei  21743  uffix  21772  neiflim  21825  hausflim  21832  flimcf  21833  flimclslem  21835  cnpflf2  21851  cnpflf  21852  fclsfnflim  21878  ustneism  22074  ustuqtop5  22096  neipcfilu  22147  dv11cn  23809  noextendseq  31945  scutbdaylt  32047  elpaddat  35408  elpadd2at  35410  snn0d  39572  ovnovollem3  41193
 Copyright terms: Public domain W3C validator