theorem sseq0 (A B: set): $ A C_ B -> B == 0 -> A == 0 $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ss02 | A C_ 0 <-> A == 0 |
|
| 2 | sseq2 | B == 0 -> (A C_ B <-> A C_ 0) |
|
| 3 | 2 | bi1d | B == 0 -> A C_ B -> A C_ 0 |
| 4 | 3 | com12 | A C_ B -> B == 0 -> A C_ 0 |
| 5 | 1, 4 | syl6ib | A C_ B -> B == 0 -> A == 0 |