Theorem snnzg 4103

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 4014	. 2 |- ( A e. V -> A e. { A } )
2		ne0i 3754	. 2 |- ( A e. { A } -> { A } =/= (/) )
3	1, 2	syl 16	1 |- ( A e. V -> { A } =/= (/) )

Syntax hints:   -> wi 4   e. wcel 1758   =/= wne 2648   (/)c0 3748   {csn 3988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-nul 3749  df-sn 3989

This theorem is referenced by:  snnz  4104  0nelop  4692  frirr  4808  frsn  5020  xpimasnOLD  5395  1stconst  6774  2ndconst  6775  fczsupp0  6831  hashge3el3dif  12308  pwsbas  14547  pwsle  14552  trnei  19600  uffix  19629  neiflim  19682  hausflim  19689  flimcf  19690  flimclslem  19692  cnpflf2  19708  cnpflf  19709  fclsfnflim  19735  ustneism  19933  ustuqtop5  19955  neipcfilu  20006  dv11cn  21609  usgra1v  23480  elpaddat  33806  elpadd2at  33808