Theorem snnzg 4665

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2934  ∅c0 4211  {csn 4516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-dif 3846  df-nul 4212  df-sn 4517

This theorem is referenced by:  snn0d  4666  snnz  4667  frirr  5502  frsn  5610  omsucne  7619  1stconst  7823  2ndconst  7824  fczsupp0  7890  hashge3el3dif  13940  pwsbas  16865  pwsle  16870  trnei  22645  uffix  22674  neiflim  22727  flimclslem  22737  fclsfnflim  22780  ustneism  22977  ustuqtop5  22999  dv11cn  24755  snsssng  30436  cosnop  30605  noextendseq  33515  scutbdaylt  33657  lltropt  33701  elpadd2at  37465