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 4356 | . . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) | |
2 | 1 | ex 415 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 = ∅ → 𝐴 = ∅)) |
3 | 2 | necon3d 3040 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ≠ ∅ → 𝐵 ≠ ∅)) |
4 | 3 | imp 409 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐵 ≠ ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1536 ≠ wne 3019 ⊆ wss 3939 ∅c0 4294 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-ne 3020 df-dif 3942 df-in 3946 df-ss 3955 df-nul 4295 |
This theorem is referenced by: unixp0 6137 frxp 7823 onfununi 7981 carddomi2 9402 fin23lem21 9764 wunex2 10163 vdwmc2 16318 gsumval2 17899 subgint 18306 subrgint 19560 hausnei2 21964 fbun 22451 fbfinnfr 22452 filuni 22496 isufil2 22519 ufileu 22530 filufint 22531 fmfnfm 22569 hausflim 22592 flimclslem 22595 fclsneii 22628 fclsbas 22632 fclsrest 22635 fclscf 22636 fclsfnflim 22638 flimfnfcls 22639 fclscmp 22641 ufilcmp 22643 isfcf 22645 fcfnei 22646 clssubg 22720 ustfilxp 22824 metustfbas 23170 restmetu 23183 reperflem 23429 metdseq0 23465 relcmpcmet 23924 bcthlem5 23934 minveclem4a 24036 dvlip 24593 wlkvtxiedg 27409 imadifxp 30354 bnj970 32223 frmin 33088 neibastop1 33711 neibastop2 33713 heibor1lem 35091 isnumbasabl 39712 dfacbasgrp 39714 ioossioobi 41799 islptre 41906 stoweidlem35 42327 stoweidlem39 42331 fourierdlem46 42444 nzerooringczr 44350 |
Copyright terms: Public domain | W3C validator |