Theorem snnzg 4774

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2940  ∅c0 4333  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-dif 3954  df-nul 4334  df-sn 4627

This theorem is referenced by:  snn0d  4775  snnz  4776  frirr  5661  frsn  5773  omsucne  7906  1stconst  8125  2ndconst  8126  fczsupp0  8218  hashge3el3dif  14526  pwsbas  17532  pwsle  17537  trnei  23900  uffix  23929  neiflim  23982  flimclslem  23992  fclsfnflim  24035  ustneism  24232  ustuqtop5  24254  dv11cn  26040  noextendseq  27712  scutbdaylt  27863  lltropt  27911  snsssng  32533  cosnop  32704  elpadd2at  39808  onnog  43442  onnobdayg  43443  bdaybndbday  43445