![]() |
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 4136. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ssdifd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
sscond | ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssdifd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | sscon 4136 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∖ cdif 3943 ⊆ wss 3946 |
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 3949 df-in 3953 df-ss 3963 |
This theorem is referenced by: ssdif2d 4141 eldifeldifsn 4812 fin23lem26 10315 isercoll2 15610 fctop 22488 ntrss 22540 iunconnlem 22912 clsconn 22915 regr1lem 23224 blcld 23995 rrxdstprj1 24907 voliunlem1 25048 elrspunidl 32503 carsgclctunlem2 33255 salexct 44984 meaiininclem 45136 carageniuncllem2 45172 seposep 47459 |
Copyright terms: Public domain | W3C validator |