![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sscond | Structured version Visualization version GIF version |
Description: If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4139. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ssdifd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
sscond | ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssdifd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | sscon 4139 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∖ cdif 3946 ⊆ wss 3949 |
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 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-dif 3952 df-in 3956 df-ss 3966 |
This theorem is referenced by: ssdif2d 4144 eldifeldifsn 4815 fin23lem26 10320 isercoll2 15615 fctop 22507 ntrss 22559 iunconnlem 22931 clsconn 22934 regr1lem 23243 blcld 24014 rrxdstprj1 24926 voliunlem1 25067 elrspunidl 32546 carsgclctunlem2 33318 salexct 45050 meaiininclem 45202 carageniuncllem2 45238 seposep 47558 |
Copyright terms: Public domain | W3C validator |