Theorem snnzg 4150

Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.)

Assertion

Ref	Expression
snnzg	|- ( A e. V -> { A } =/= (/) )

Proof of Theorem snnzg

Step	Hyp	Ref	Expression
1		snidg 4059	. 2 |- ( A e. V -> A e. { A } )
2		ne0i 3796	. 2 |- ( A e. { A } -> { A } =/= (/) )
3	1, 2	syl 16	1 |- ( A e. V -> { A } =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1767   =/= wne 2662   (/)c0 3790   {csn 4033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3120  df-dif 3484  df-nul 3791  df-sn 4034

This theorem is referenced by:  snnz  4151  0nelop  4743  frirr  4862  frsn  5076  xpimasnOLD  5459  1stconst  6883  2ndconst  6884  fczsupp0  6941  hashge3el3dif  12505  pwsbas  14759  pwsle  14764  trnei  20261  uffix  20290  neiflim  20343  hausflim  20350  flimcf  20351  flimclslem  20353  cnpflf2  20369  cnpflf  20370  fclsfnflim  20396  ustneism  20594  ustuqtop5  20616  neipcfilu  20667  dv11cn  22270  usgra1v  24204  elpaddat  34956  elpadd2at  34958