Theorem snnzg 4726

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

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

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 3906  df-nul 4285  df-sn 4578

This theorem is referenced by:  snn0d  4727  snnz  4728  frirr  5595  frsn  5707  omsucne  7818  1stconst  8033  2ndconst  8034  fczsupp0  8126  hashge3el3dif  14394  pwsbas  17391  pwsle  17396  trnei  23777  uffix  23806  neiflim  23859  flimclslem  23869  fclsfnflim  23912  ustneism  24109  ustuqtop5  24131  dv11cn  25904  noextendseq  27577  scutbdaylt  27729  eqscut3  27735  lltropt  27786  snsssng  32458  cosnop  32637  elpadd2at  39789  onnog  43406  onnobdayg  43407  bdaybndbday  43409