Theorem snnzg 4729

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2930  ∅c0 4283  {csn 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-dif 3902  df-nul 4284  df-sn 4579

This theorem is referenced by:  snn0d  4730  snnz  4731  frirr  5598  frsn  5710  omsucne  7825  1stconst  8040  2ndconst  8041  fczsupp0  8133  hashge3el3dif  14408  pwsbas  17405  pwsle  17411  trnei  23834  uffix  23863  neiflim  23916  flimclslem  23926  fclsfnflim  23969  ustneism  24166  ustuqtop5  24187  dv11cn  25960  noextendseq  27633  scutbdaylt  27786  eqscut3  27792  lltropt  27844  snsssng  32538  cosnop  32723  elpadd2at  40005  onnog  43612  onnobdayg  43613  bdaybndbday  43615