Theorem snnzg 4088

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

Syntax hints:   -> wi 4   e. wcel 1886   =/= wne 2621   (/)c0 3730   {csn 3967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-v 3046  df-dif 3406  df-nul 3731  df-sn 3968

This theorem is referenced by:  snnz  4089  0nelop  4690  frirr  4810  frsn  4904  1stconst  6881  2ndconst  6882  fczsupp0  6941  hashge3el3dif  12639  pwsbas  15378  pwsle  15383  trnei  20900  uffix  20929  neiflim  20982  hausflim  20989  flimcf  20990  flimclslem  20992  cnpflf2  21008  cnpflf  21009  fclsfnflim  21035  ustneism  21231  ustuqtop5  21253  neipcfilu  21304  dv11cn  22946  usgra1v  25110  elpaddat  33363  elpadd2at  33365  usgr1vr  39312