Theorem snnzg 4718

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2932  ∅c0 4273  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3892  df-nul 4274  df-sn 4568

This theorem is referenced by:  snn0d  4719  snnz  4720  frirr  5607  frsn  5719  omsucne  7836  1stconst  8050  2ndconst  8051  fczsupp0  8143  hashge3el3dif  14449  pwsbas  17450  pwsle  17456  trnei  23857  uffix  23886  neiflim  23939  flimclslem  23949  fclsfnflim  23992  ustneism  24189  ustuqtop5  24210  dv11cn  25968  noextendseq  27631  cutbdaylt  27790  eqcuts3  27796  lltr  27854  snsssng  32584  cosnop  32768  mh-inf3sn  36724  elpadd2at  40252  onnoxpg  43856  onnobdayg  43857  bdaybndbday  43859