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

Theorem snnzg 4665
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 4550 . 2 (𝐴𝑉𝐴 ∈ {𝐴})
21ne0d 4224 1 (𝐴𝑉 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  wne 2934  c0 4211  {csn 4516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-dif 3846  df-nul 4212  df-sn 4517
This theorem is referenced by:  snn0d  4666  snnz  4667  frirr  5502  frsn  5610  omsucne  7619  1stconst  7823  2ndconst  7824  fczsupp0  7890  hashge3el3dif  13940  pwsbas  16865  pwsle  16870  trnei  22645  uffix  22674  neiflim  22727  flimclslem  22737  fclsfnflim  22780  ustneism  22977  ustuqtop5  22999  dv11cn  24755  snsssng  30436  cosnop  30605  noextendseq  33515  scutbdaylt  33657  lltropt  33701  elpadd2at  37465
  Copyright terms: Public domain W3C validator