Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssn0 | Structured version Visualization version GIF 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 3927 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | |
2 | 1 | ex 449 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅)) |
3 | 2 | necon3d 2803 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅)) |
4 | 3 | imp 444 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ≠ wne 2780 ⊆ wss 3540 ∅c0 3874 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 df-nul 3875 |
This theorem is referenced by: unixp0 5586 frxp 7174 onfununi 7325 carddomi2 8679 fin23lem21 9044 wunex2 9439 vdwmc2 15521 gsumval2 17103 subgint 17441 subrgint 18625 hausnei2 20967 fbun 21454 fbfinnfr 21455 filuni 21499 isufil2 21522 ufileu 21533 filufint 21534 fmfnfm 21572 hausflim 21595 flimclslem 21598 fclsneii 21631 fclsbas 21635 fclsrest 21638 fclscf 21639 fclsfnflim 21641 flimfnfcls 21642 fclscmp 21644 ufilcmp 21646 isfcf 21648 fcfnei 21649 clssubg 21722 ustfilxp 21826 metustfbas 22172 restmetu 22185 reperflem 22429 metdseq0 22465 relcmpcmet 22923 bcthlem5 22933 minveclem4a 23009 dvlip 23560 imadifxp 28796 bnj970 30271 frmin 30983 neibastop1 31524 neibastop2 31526 heibor1lem 32778 isnumbasabl 36695 dfacbasgrp 36697 ioossioobi 38590 islptre 38686 stoweidlem35 38928 stoweidlem39 38932 fourierdlem46 39045 1wlkvtxiedg 40829 nzerooringczr 41864 |
Copyright terms: Public domain | W3C validator |