Theorem snnzg 4734

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  ∅c0 4292  {csn 4585

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-dif 3914  df-nul 4293  df-sn 4586

This theorem is referenced by:  snn0d  4735  snnz  4736  frirr  5607  frsn  5719  omsucne  7841  1stconst  8056  2ndconst  8057  fczsupp0  8149  hashge3el3dif  14428  pwsbas  17426  pwsle  17431  trnei  23812  uffix  23841  neiflim  23894  flimclslem  23904  fclsfnflim  23947  ustneism  24144  ustuqtop5  24166  dv11cn  25939  noextendseq  27612  scutbdaylt  27764  eqscut3  27770  lltropt  27821  snsssng  32493  cosnop  32668  elpadd2at  39793  onnog  43411  onnobdayg  43412  bdaybndbday  43414