| 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 4144. (Contributed by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| ssdifd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| Ref | Expression |
|---|---|
| ssdifd | ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssdifd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
| 2 | ssdif 4144 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∖ cdif 3948 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-dif 3954 df-ss 3968 |
| This theorem is referenced by: ssdif2d 4148 domunsncan 9112 fin1a2lem13 10452 seqcoll2 14504 rpnnen2lem11 16260 coprmprod 16698 mrieqv2d 17682 mrissmrid 17684 mreexexlem4d 17690 acsfiindd 18598 subdrgint 20804 lsppratlem3 21151 lsppratlem4 21152 f1lindf 21842 lpss3 23152 lpcls 23372 fin1aufil 23940 rrxmval 25439 rrxmetlem 25441 uniioombllem3 25620 i1fmul 25731 itg1addlem4 25734 itg1climres 25749 limciun 25929 ig1peu 26214 ig1pdvds 26219 fusgreghash2wspv 30354 indsumin 32847 chnind 33001 pmtrcnel2 33110 pmtrcnelor 33111 tocyccntz 33164 elrspunidl 33456 elrspunsn 33457 sitgclg 34344 mthmpps 35587 poimirlem11 37638 poimirlem12 37639 poimirlem15 37642 dochfln0 41479 lcfl6 41502 lcfrlem16 41560 hdmaprnlem4N 41855 tfsconcatlem 43349 caragendifcl 46529 |
| Copyright terms: Public domain | W3C validator |