Theorem snnzg 4719

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274  {csn 4568

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-dif 3893  df-nul 4275  df-sn 4569

This theorem is referenced by:  snn0d  4720  snnz  4721  frirr  5601  frsn  5713  omsucne  7830  1stconst  8044  2ndconst  8045  fczsupp0  8137  hashge3el3dif  14443  pwsbas  17444  pwsle  17450  trnei  23870  uffix  23899  neiflim  23952  flimclslem  23962  fclsfnflim  24005  ustneism  24202  ustuqtop5  24223  dv11cn  25981  noextendseq  27648  cutbdaylt  27807  eqcuts3  27813  lltr  27871  snsssng  32602  cosnop  32786  mh-inf3sn  36743  elpadd2at  40269  onnoxpg  43877  onnobdayg  43878  bdaybndbday  43880