![]() |
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 3971 | . . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅)) | |
2 | ss0 4359 | . . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | |
3 | 1, 2 | syl6bi 253 | . 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅)) |
4 | 3 | impcom 409 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ⊆ wss 3911 ∅c0 4283 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3448 df-dif 3914 df-in 3918 df-ss 3928 df-nul 4284 |
This theorem is referenced by: ssn0 4361 ssdifin0 4444 disjxiun 5103 f1un 6805 fsetexb 8803 undomOLD 9005 infn0 9252 fieq0 9358 infdifsn 9594 cantnff 9611 tc00 9685 hashun3 14285 strleun 17030 dmdprdsplit2lem 19825 2idlval 20706 ocvval 21074 pjfval 21115 opsrle 21451 pf1rcl 21718 en2top 22338 nrmsep 22711 isnrm3 22713 regsep2 22730 xkohaus 23007 kqdisj 23086 regr1lem 23093 alexsublem 23398 reconnlem1 24192 metdstri 24217 iundisj2 24916 left0s 27225 right0s 27226 0clwlk0 29079 disjxpin 31509 iundisj2f 31511 iundisj2fi 31703 cvmsss2 33871 cldbnd 34801 cntotbnd 36258 nna4b4nsq 41001 mapfzcons1 41043 onfrALTlem2 42835 onfrALTlem2VD 43178 nnuzdisj 43596 ssdisjd 46899 ssdisjdr 46900 sepnsepolem2 46962 sepnsepo 46963 |
Copyright terms: Public domain | W3C validator |