Theorem snnzg 4707

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2942  ∅c0 4253  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-dif 3886  df-nul 4254  df-sn 4559

This theorem is referenced by:  snn0d  4708  snnz  4709  frirr  5557  frsn  5665  omsucne  7706  1stconst  7911  2ndconst  7912  fczsupp0  7980  hashge3el3dif  14128  pwsbas  17115  pwsle  17120  trnei  22951  uffix  22980  neiflim  23033  flimclslem  23043  fclsfnflim  23086  ustneism  23283  ustuqtop5  23305  dv11cn  25070  snsssng  30761  cosnop  30930  noextendseq  33797  scutbdaylt  33939  lltropt  33983  elpadd2at  37747