Theorem snnzg 4750

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 4636	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
2	1	ne0d 4317	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2932  ∅c0 4308  {csn 4601

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 2707

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 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-dif 3929  df-nul 4309  df-sn 4602

This theorem is referenced by:  snn0d  4751  snnz  4752  frirr  5630  frsn  5742  omsucne  7880  1stconst  8099  2ndconst  8100  fczsupp0  8192  hashge3el3dif  14505  pwsbas  17501  pwsle  17506  trnei  23830  uffix  23859  neiflim  23912  flimclslem  23922  fclsfnflim  23965  ustneism  24162  ustuqtop5  24184  dv11cn  25958  noextendseq  27631  scutbdaylt  27782  lltropt  27836  snsssng  32495  cosnop  32672  elpadd2at  39825  onnog  43453  onnobdayg  43454  bdaybndbday  43456