Theorem snnzg 4742

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960  ∅c0 4286  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3909  df-nul 4287  df-sn 4592

This theorem is used by:  snn0d  4743  snnz  4744  frirr  5639  frsn  5751  omsucne  7887  1stconst  8101  2ndconst  8102  fczsupp0  8195  hashge3el3dif  14544  pwsbas  17564  pwsle  17570  trnei  24102  uffix  24131  neiflim  24184  flimclslem  24194  fclsfnflim  24237  ustneism  24434  ustuqtop5  24455  dv11cn  26213  noextendseq  27884  cutbdaylt  28044  eqcuts3  28050  lltr  28108  snsssng  32933  cosnop  33113  mh-inf3sn  37112  elpadd2at  40640  onnoxpg  44215  onnobdayg  44216  bdaybndbday  44218