Theorem snnzg 4778

Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)

Assertion

Ref	Expression
snnzg	⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)

Proof of Theorem snnzg

Step	Hyp	Ref	Expression
1		snidg 4664	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
2	1	ne0d 4347	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2937  ∅c0 4338  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-dif 3965  df-nul 4339  df-sn 4631

This theorem is referenced by:  snn0d  4779  snnz  4780  frirr  5664  frsn  5775  omsucne  7905  1stconst  8123  2ndconst  8124  fczsupp0  8216  hashge3el3dif  14522  pwsbas  17533  pwsle  17538  trnei  23915  uffix  23944  neiflim  23997  flimclslem  24007  fclsfnflim  24050  ustneism  24247  ustuqtop5  24269  dv11cn  26054  noextendseq  27726  scutbdaylt  27877  lltropt  27925  snsssng  32541  cosnop  32709  elpadd2at  39788  onnog  43418  onnobdayg  43419  bdaybndbday  43421