Theorem snnzg 4731

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2932  ∅c0 4285  {csn 4580

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3904  df-nul 4286  df-sn 4581

This theorem is referenced by:  snn0d  4732  snnz  4733  frirr  5600  frsn  5712  omsucne  7827  1stconst  8042  2ndconst  8043  fczsupp0  8135  hashge3el3dif  14410  pwsbas  17407  pwsle  17413  trnei  23836  uffix  23865  neiflim  23918  flimclslem  23928  fclsfnflim  23971  ustneism  24168  ustuqtop5  24189  dv11cn  25962  noextendseq  27635  cutbdaylt  27794  eqcuts3  27800  lltr  27858  snsssng  32589  cosnop  32774  elpadd2at  40076  onnoxpg  43680  onnobdayg  43681  bdaybndbday  43683