![]() |
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 4006 | . . 3 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅)) | |
2 | ss0 4403 | . . 3 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | |
3 | 1, 2 | biimtrdi 252 | . 2 ⊢ (𝐵 = ∅ → (𝐴 ⊆ 𝐵 → 𝐴 = ∅)) |
4 | 3 | impcom 406 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ⊆ wss 3947 ∅c0 4325 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-dif 3950 df-ss 3964 df-nul 4326 |
This theorem is referenced by: ssn0 4405 ssdifin0 4490 disjxiun 5150 f1un 6863 fsetexb 8893 undomOLD 9098 infn0 9341 fieq0 9464 infdifsn 9700 cantnff 9717 tc00 9791 hashun3 14401 strleun 17159 dmdprdsplit2lem 20045 2idlval 21240 ocvval 21663 pjfval 21704 opsrle 22054 pf1rcl 22340 en2top 22979 nrmsep 23352 isnrm3 23354 regsep2 23371 xkohaus 23648 kqdisj 23727 regr1lem 23734 alexsublem 24039 reconnlem1 24833 metdstri 24858 iundisj2 25569 left0s 27916 right0s 27917 0clwlk0 30065 disjxpin 32508 iundisj2f 32510 iundisj2fi 32699 1arithufdlem4 33422 cvmsss2 35102 cldbnd 36038 cntotbnd 37497 nna4b4nsq 42314 mapfzcons1 42374 onfrALTlem2 44222 onfrALTlem2VD 44565 nnuzdisj 44970 ssdisjd 48193 ssdisjdr 48194 sepnsepolem2 48256 sepnsepo 48257 |
Copyright terms: Public domain | W3C validator |