![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssn0 | Structured version Visualization version Unicode version |
Description: A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.) |
Ref | Expression |
---|---|
ssn0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq0 3778 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 440 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | necon3d 2657 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | imp 435 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-v 3059 df-dif 3419 df-in 3423 df-ss 3430 df-nul 3744 |
This theorem is referenced by: unixp0 5389 frxp 6933 onfununi 7086 carddomi2 8430 fin23lem21 8795 wunex2 9189 vdwmc2 14978 gsumval2 16572 subgint 16890 subrgint 18079 hausnei2 20418 fbun 20904 fbfinnfr 20905 filuni 20949 isufil2 20972 ufileu 20983 filufint 20984 fmfnfm 21022 hausflim 21045 flimclslem 21048 fclsneii 21081 fclsbas 21085 fclsrest 21088 fclscf 21089 fclsfnflim 21091 flimfnfcls 21092 fclscmp 21094 ufilcmp 21096 isfcf 21098 fcfnei 21099 clssubg 21172 ustfilxp 21276 metustfbas 21621 restmetu 21634 reperflem 21885 metdseq0 21920 metdseq0OLD 21935 relcmpcmet 22335 bcthlem5 22345 minveclem4a 22421 minveclem4aOLD 22433 dvlip 22994 imadifxp 28261 bnj970 29807 frmin 30529 neibastop1 31064 neibastop2 31066 heibor1lem 32186 isnumbasabl 36010 dfacbasgrp 36012 ioossioobi 37656 islptre 37737 stoweidlem35 37934 stoweidlem39 37938 fourierdlem46 38054 1wlkvtxiedg 39687 nzerooringczr 40347 |
Copyright terms: Public domain | W3C validator |