Theorem snnzg 4745

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

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  ∅c0 4294  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-dif 3916  df-nul 4295  df-sn 4595

This theorem is referenced by:  snn0d  4746  snnz  4747  frirr  5638  frsn  5750  omsucne  7881  1stconst  8095  2ndconst  8096  fczsupp0  8189  hashge3el3dif  14524  pwsbas  17540  pwsle  17546  trnei  24018  uffix  24047  neiflim  24100  flimclslem  24110  fclsfnflim  24153  ustneism  24350  ustuqtop5  24371  dv11cn  26129  noextendseq  27797  cutbdaylt  27957  eqcuts3  27963  lltr  28021  snsssng  32801  cosnop  32981  mh-inf3sn  36942  elpadd2at  40470  onnoxpg  44047  onnobdayg  44048  bdaybndbday  44050