Theorem snnzg 4770

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

Syntax hints:   → wi 4   ∈ wcel 2098   ≠ wne 2932  ∅c0 4314  {csn 4620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-dif 3943  df-nul 4315  df-sn 4621

This theorem is referenced by:  snn0d  4771  snnz  4772  frirr  5643  frsn  5753  omsucne  7867  1stconst  8080  2ndconst  8081  fczsupp0  8172  hashge3el3dif  14443  pwsbas  17429  pwsle  17434  trnei  23706  uffix  23735  neiflim  23788  flimclslem  23798  fclsfnflim  23841  ustneism  24038  ustuqtop5  24060  dv11cn  25844  noextendseq  27504  scutbdaylt  27655  lltropt  27703  snsssng  32176  cosnop  32341  elpadd2at  39133  onnog  42635  onnobdayg  42636  bdaybndbday  42638