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 3975 | . . . 4 | |
2 | 1 | ex 450 | . . 3 |
3 | 2 | necon3d 2815 | . 2 |
4 | 3 | imp 445 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wceq 1483 wne 2794 wss 3574 c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-v 3202 df-dif 3577 df-in 3581 df-ss 3588 df-nul 3916 |
This theorem is referenced by: unixp0 5669 frxp 7287 onfununi 7438 carddomi2 8796 fin23lem21 9161 wunex2 9560 vdwmc2 15683 gsumval2 17280 subgint 17618 subrgint 18802 hausnei2 21157 fbun 21644 fbfinnfr 21645 filuni 21689 isufil2 21712 ufileu 21723 filufint 21724 fmfnfm 21762 hausflim 21785 flimclslem 21788 fclsneii 21821 fclsbas 21825 fclsrest 21828 fclscf 21829 fclsfnflim 21831 flimfnfcls 21832 fclscmp 21834 ufilcmp 21836 isfcf 21838 fcfnei 21839 clssubg 21912 ustfilxp 22016 metustfbas 22362 restmetu 22375 reperflem 22621 metdseq0 22657 relcmpcmet 23115 bcthlem5 23125 minveclem4a 23201 dvlip 23756 wlkvtxiedg 26520 imadifxp 29414 bnj970 31017 frmin 31739 neibastop1 32354 neibastop2 32356 heibor1lem 33608 isnumbasabl 37676 dfacbasgrp 37678 ioossioobi 39743 islptre 39851 stoweidlem35 40252 stoweidlem39 40256 fourierdlem46 40369 nzerooringczr 42072 |
Copyright terms: Public domain | W3C validator |