Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssdifd | Structured version Visualization version GIF version |
Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 3707. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ssdifd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
ssdifd | ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssdifd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | ssdif 3707 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∖ cdif 3537 ⊆ wss 3540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 |
This theorem is referenced by: ssdif2d 3711 domunsncan 7945 fin1a2lem13 9117 seqcoll2 13106 rpnnen2lem11 14792 coprmprod 15213 mrieqv2d 16122 mrissmrid 16124 mreexexlem4d 16130 acsfiindd 17000 lsppratlem3 18970 lsppratlem4 18971 f1lindf 19980 lpss3 20758 lpcls 20978 fin1aufil 21546 rrxmval 22996 rrxmetlem 22998 uniioombllem3 23159 i1fmul 23269 itg1addlem4 23272 itg1climres 23287 limciun 23464 ig1peu 23735 ig1pdvds 23740 nbgrassovt 25964 usgreghash2spotv 26593 sitgclg 29731 mthmpps 30733 poimirlem11 32590 poimirlem12 32591 poimirlem15 32594 dochfln0 35784 lcfl6 35807 lcfrlem16 35865 hdmaprnlem4N 36163 caragendifcl 39404 fusgreghash2wspv 41499 |
Copyright terms: Public domain | W3C validator |