Theorem snnzg 4706

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 4270	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2119   ≠ wne 2934  ∅c0 4261  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-dif 3886  df-nul 4262  df-sn 4556

This theorem is referenced by:  snn0d  4707  snnz  4708  frirr  5594  frsn  5706  omsucne  7825  1stconst  8039  2ndconst  8040  fczsupp0  8133  hashge3el3dif  14440  pwsbas  17441  pwsle  17447  trnei  23875  uffix  23904  neiflim  23957  flimclslem  23967  fclsfnflim  24010  ustneism  24207  ustuqtop5  24228  dv11cn  25986  noextendseq  27649  cutbdaylt  27808  eqcuts3  27814  lltr  27872  snsssng  32602  cosnop  32787  mh-inf3sn  36770  elpadd2at  40298  onnoxpg  43873  onnobdayg  43874  bdaybndbday  43876