Theorem snnzg 4735

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2956  ∅c0 4279  {csn 4584

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3902  df-nul 4280  df-sn 4585

This theorem is used by:  snn0d  4736  snnz  4737  frirr  5627  frsn  5739  omsucne  7896  1stconst  8111  2ndconst  8112  fczsupp0  8210  hashge3el3dif  14632  pwsbas  17658  pwsle  17664  trnei  24211  uffix  24240  neiflim  24293  flimclslem  24303  fclsfnflim  24346  ustneism  24543  ustuqtop5  24564  dv11cn  26321  noextendseq  28024  cutbdaylt  28184  eqcuts3  28190  lltr  28248  snsssng  33110  cosnop  33288  mh-inf3sn  37330  elpadd2at  40863  onnoxpg  44429  onnobdayg  44430  bdaybndbday  44432