![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sseq0 | Structured version Visualization version GIF version |
Description: A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
sseq0 | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3823 | . . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅)) | |
2 | ss0 4170 | . . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | |
3 | 1, 2 | syl6bi 245 | . 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅)) |
4 | 3 | impcom 397 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ⊆ wss 3769 ∅c0 4115 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-v 3387 df-dif 3772 df-in 3776 df-ss 3783 df-nul 4116 |
This theorem is referenced by: ssn0 4172 ssdifin0 4244 disjxiun 4840 undom 8290 fieq0 8569 infdifsn 8804 cantnff 8821 tc00 8874 hashun3 13423 strleun 16293 xpsc0 16535 xpsc1 16536 dmdprdsplit2lem 18760 2idlval 19556 opsrle 19798 pf1rcl 20035 ocvval 20336 pjfval 20375 en2top 21118 nrmsep 21490 isnrm3 21492 regsep2 21509 xkohaus 21785 kqdisj 21864 regr1lem 21871 alexsublem 22176 reconnlem1 22957 metdstri 22982 iundisj2 23657 0clwlk0 27476 disjxpin 29918 iundisj2f 29920 iundisj2fi 30074 cvmsss2 31773 cldbnd 32833 cntotbnd 34082 mapfzcons1 38066 onfrALTlem2 39532 onfrALTlem2VD 39885 nnuzdisj 40315 |
Copyright terms: Public domain | W3C validator |