Theorem snnzg 4740

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

Syntax hints:   → wi 4   ∈ wcel 2143   ≠ wne 2958  ∅c0 4286  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 3908  df-nul 4287  df-sn 4590

This theorem is referenced by:  snn0d  4741  snnz  4742  frirr  5637  frsn  5749  omsucne  7877  1stconst  8091  2ndconst  8092  fczsupp0  8185  hashge3el3dif  14520  pwsbas  17535  pwsle  17541  trnei  24049  uffix  24078  neiflim  24131  flimclslem  24141  fclsfnflim  24184  ustneism  24381  ustuqtop5  24402  dv11cn  26160  noextendseq  27831  cutbdaylt  27991  eqcuts3  27997  lltr  28055  snsssng  32860  cosnop  33040  mh-inf3sn  37073  elpadd2at  40600  onnoxpg  44175  onnobdayg  44176  bdaybndbday  44178