| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ssdifss | Structured version Visualization version GIF version | ||
| Description: Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.) |
| Ref | Expression |
|---|---|
| ssdifss | ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | difss 4088 | . 2 ⊢ (𝐴 ∖ 𝐶) ⊆ 𝐴 | |
| 2 | sstr 3942 | . 2 ⊢ (((𝐴 ∖ 𝐶) ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∖ 𝐶) ⊆ 𝐵) | |
| 3 | 1, 2 | mpan 690 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∖ cdif 3898 ⊆ wss 3901 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1544 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-v 3442 df-dif 3904 df-ss 3918 |
| This theorem is referenced by: ssdifssd 4099 xrsupss 13224 xrinfmss 13225 rpnnen2lem12 16150 lpval 23083 lpdifsn 23087 islp2 23089 lpcls 23308 mblfinlem3 37860 mblfinlem4 37861 voliunnfl 37865 redvmptabs 42625 ssdifcl 43822 sssymdifcl 43823 supxrmnf2 45687 infxrpnf2 45717 fourierdlem102 46462 fourierdlem114 46474 lindslinindimp2lem4 48717 lindslinindsimp2lem5 48718 lindslinindsimp2 48719 lincresunit3 48737 |
| Copyright terms: Public domain | W3C validator |