Theorem snnzg 4710

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

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2943  ∅c0 4256  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-dif 3890  df-nul 4257  df-sn 4562

This theorem is referenced by:  snn0d  4711  snnz  4712  frirr  5566  frsn  5674  omsucne  7731  1stconst  7940  2ndconst  7941  fczsupp0  8009  hashge3el3dif  14200  pwsbas  17198  pwsle  17203  trnei  23043  uffix  23072  neiflim  23125  flimclslem  23135  fclsfnflim  23178  ustneism  23375  ustuqtop5  23397  dv11cn  25165  snsssng  30860  cosnop  31028  noextendseq  33870  scutbdaylt  34012  lltropt  34056  elpadd2at  37820