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

Theorem snnzg 4285
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 4184 . 2 (𝐴𝑉𝐴 ∈ {𝐴})
2 ne0i 3903 . 2 (𝐴 ∈ {𝐴} → {𝐴} ≠ ∅)
31, 2syl 17 1 (𝐴𝑉 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wne 2790  c0 3897  {csn 4155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-v 3192  df-dif 3563  df-nul 3898  df-sn 4156
This theorem is referenced by:  snnz  4286  0nelop  4930  frirr  5061  frsn  5160  1stconst  7225  2ndconst  7226  fczsupp0  7284  hashge3el3dif  13222  pwsbas  16087  pwsle  16092  trnei  21636  uffix  21665  neiflim  21718  hausflim  21725  flimcf  21726  flimclslem  21728  cnpflf2  21744  cnpflf  21745  fclsfnflim  21771  ustneism  21967  ustuqtop5  21989  neipcfilu  22040  dv11cn  23702  elpaddat  34609  elpadd2at  34611  snn0d  38780  ovnovollem3  40209
  Copyright terms: Public domain W3C validator