![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > snnzg | Structured version Visualization version Unicode version |
Description: The singleton of a set is not empty. (Contributed by NM, 14-Dec-2008.) |
Ref | Expression |
---|---|
snnzg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snidg 3993 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ne0i 3736 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 |
Copyright terms: Public domain | W3C validator |