![]() |
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 4008 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | |
2 | 1 | ex 449 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅)) |
3 | 2 | necon3d 2844 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅)) |
4 | 3 | imp 444 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1523 ≠ wne 2823 ⊆ wss 3607 ∅c0 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-v 3233 df-dif 3610 df-in 3614 df-ss 3621 df-nul 3949 |
This theorem is referenced by: unixp0 5707 frxp 7332 onfununi 7483 carddomi2 8834 fin23lem21 9199 wunex2 9598 vdwmc2 15730 gsumval2 17327 subgint 17665 subrgint 18850 hausnei2 21205 fbun 21691 fbfinnfr 21692 filuni 21736 isufil2 21759 ufileu 21770 filufint 21771 fmfnfm 21809 hausflim 21832 flimclslem 21835 fclsneii 21868 fclsbas 21872 fclsrest 21875 fclscf 21876 fclsfnflim 21878 flimfnfcls 21879 fclscmp 21881 ufilcmp 21883 isfcf 21885 fcfnei 21886 clssubg 21959 ustfilxp 22063 metustfbas 22409 restmetu 22422 reperflem 22668 metdseq0 22704 relcmpcmet 23161 bcthlem5 23171 minveclem4a 23247 dvlip 23801 wlkvtxiedg 26576 imadifxp 29540 bnj970 31143 frmin 31867 neibastop1 32479 neibastop2 32481 heibor1lem 33738 isnumbasabl 37993 dfacbasgrp 37995 ioossioobi 40061 islptre 40169 stoweidlem35 40570 stoweidlem39 40574 fourierdlem46 40687 nzerooringczr 42397 |
Copyright terms: Public domain | W3C validator |