Theorem snnzg 4670

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2987  ∅c0 4243  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-dif 3884  df-nul 4244  df-sn 4526

This theorem is referenced by:  snn0d  4671  snnz  4672  0nelop  5351  frirr  5496  frsn  5603  omsucne  7578  1stconst  7778  2ndconst  7779  fczsupp0  7842  hashge3el3dif  13840  pwsbas  16752  pwsle  16757  trnei  22497  uffix  22526  neiflim  22579  hausflim  22586  flimcf  22587  flimclslem  22589  cnpflf2  22605  cnpflf  22606  fclsfnflim  22632  ustneism  22829  ustuqtop5  22851  neipcfilu  22902  dv11cn  24604  snsssng  30284  cosnop  30455  zarclssn  31226  noextendseq  33287  scutbdaylt  33389  elpaddat  37100  elpadd2at  37102  mnuprdlem1  40980  ovnovollem3  43297