Theorem snnzg 4308

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 4206	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})
2		ne0i 3921	. 2 ⊢ (𝐴 ∈ {𝐴} → {𝐴} ≠ ∅)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 1990   ≠ wne 2794  ∅c0 3915  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-nul 3916  df-sn 4178

This theorem is referenced by:  snnz  4309  0nelop  4960  frirr  5091  frsn  5189  1stconst  7265  2ndconst  7266  fczsupp0  7324  hashge3el3dif  13268  pwsbas  16147  pwsle  16152  trnei  21696  uffix  21725  neiflim  21778  hausflim  21785  flimcf  21786  flimclslem  21788  cnpflf2  21804  cnpflf  21805  fclsfnflim  21831  ustneism  22027  ustuqtop5  22049  neipcfilu  22100  dv11cn  23764  noextendseq  31820  scutbdaylt  31922  elpaddat  35090  elpadd2at  35092  snn0d  39258  ovnovollem3  40872