| 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 4136 | . 2 ⊢ (𝐴 ∖ 𝐶) ⊆ 𝐴 | |
| 2 | sstr 3992 | . 2 ⊢ (((𝐴 ∖ 𝐶) ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∖ 𝐶) ⊆ 𝐵) | |
| 3 | 1, 2 | mpan 690 | 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: ssdifssd 4147 xrsupss 13351 xrinfmss 13352 rpnnen2lem12 16261 lpval 23147 lpdifsn 23151 islp2 23153 lpcls 23372 mblfinlem3 37666 mblfinlem4 37667 voliunnfl 37671 redvmptabs 42390 ssdifcl 43584 sssymdifcl 43585 supxrmnf2 45444 infxrpnf2 45474 fourierdlem102 46223 fourierdlem114 46235 lindslinindimp2lem4 48378 lindslinindsimp2lem5 48379 lindslinindsimp2 48380 lincresunit3 48398 |
| Copyright terms: Public domain | W3C validator |