Theorem snnzg 4724

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928  ∅c0 4280  {csn 4573

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-dif 3900  df-nul 4281  df-sn 4574

This theorem is referenced by:  snn0d  4725  snnz  4726  frirr  5590  frsn  5702  omsucne  7815  1stconst  8030  2ndconst  8031  fczsupp0  8123  hashge3el3dif  14394  pwsbas  17391  pwsle  17396  trnei  23807  uffix  23836  neiflim  23889  flimclslem  23899  fclsfnflim  23942  ustneism  24139  ustuqtop5  24160  dv11cn  25933  noextendseq  27606  scutbdaylt  27759  eqscut3  27765  lltropt  27817  snsssng  32494  cosnop  32676  elpadd2at  39915  onnog  43532  onnobdayg  43533  bdaybndbday  43535