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

Theorem snnzg 4774
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 4660 . 2 (𝐴𝑉𝐴 ∈ {𝐴})
21ne0d 4342 1 (𝐴𝑉 → {𝐴} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wne 2940  c0 4333  {csn 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-dif 3954  df-nul 4334  df-sn 4627
This theorem is referenced by:  snn0d  4775  snnz  4776  frirr  5661  frsn  5773  omsucne  7906  1stconst  8125  2ndconst  8126  fczsupp0  8218  hashge3el3dif  14526  pwsbas  17532  pwsle  17537  trnei  23900  uffix  23929  neiflim  23982  flimclslem  23992  fclsfnflim  24035  ustneism  24232  ustuqtop5  24254  dv11cn  26040  noextendseq  27712  scutbdaylt  27863  lltropt  27911  snsssng  32533  cosnop  32704  elpadd2at  39808  onnog  43442  onnobdayg  43443  bdaybndbday  43445
  Copyright terms: Public domain W3C validator