Theorem snnzg 4496

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

Syntax hints:   → wi 4   ∈ wcel 2157   ≠ wne 2971  ∅c0 4115  {csn 4368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-v 3387  df-dif 3772  df-nul 4116  df-sn 4369

This theorem is referenced by:  snnz  4497  0nelop  5150  frirr  5289  frsn  5394  1stconst  7502  2ndconst  7503  fczsupp0  7562  hashge3el3dif  13517  pwsbas  16462  pwsle  16467  trnei  22024  uffix  22053  neiflim  22106  hausflim  22113  flimcf  22114  flimclslem  22116  cnpflf2  22132  cnpflf  22133  fclsfnflim  22159  ustneism  22355  ustuqtop5  22377  neipcfilu  22428  dv11cn  24105  noextendseq  32333  scutbdaylt  32435  elpaddat  35825  elpadd2at  35827  snn0d  40017  ovnovollem3  41618