Theorem snnzg 4738

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

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

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 3917  df-nul 4297  df-sn 4590

This theorem is referenced by:  snn0d  4739  snnz  4740  frirr  5614  frsn  5726  omsucne  7861  1stconst  8079  2ndconst  8080  fczsupp0  8172  hashge3el3dif  14452  pwsbas  17450  pwsle  17455  trnei  23779  uffix  23808  neiflim  23861  flimclslem  23871  fclsfnflim  23914  ustneism  24111  ustuqtop5  24133  dv11cn  25906  noextendseq  27579  scutbdaylt  27730  lltropt  27784  snsssng  32443  cosnop  32618  elpadd2at  39800  onnog  43418  onnobdayg  43419  bdaybndbday  43421