Theorem snnzg 4734

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2958  ∅c0 4280  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 4049  df-nul 4281  df-sn 4588

This theorem is used by:  snn0d  4735  snnz  4736  frirr  5630  frsn  5743  omsucne  7903  1stconst  8121  2ndconst  8122  fczsupp0  8221  hashge3el3dif  14642  pwsbas  17670  pwsle  17676  trnei  24223  uffix  24252  neiflim  24305  flimclslem  24315  fclsfnflim  24358  ustneism  24555  ustuqtop5  24576  dv11cn  26333  noextendseq  28036  cutbdaylt  28196  eqcuts3  28202  lltr  28260  snsssng  33164  cosnop  33342  mh-inf3sn  37457  elpadd2at  41003  onnoxpg  44570  onnobdayg  44571  bdaybndbday  44573