| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ssdif | Structured version Visualization version GIF version | ||
| Description: Difference law for subsets. (Contributed by NM, 28-May-1998.) |
| Ref | Expression |
|---|---|
| ssdif | ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssel 3977 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 2 | 1 | anim1d 611 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))) |
| 3 | eldif 3961 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)) | |
| 4 | eldif 3961 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) | |
| 5 | 2, 3, 4 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶))) |
| 6 | 5 | ssrdv 3989 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∈ wcel 2108 ∖ 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: ssdifd 4145 pssnn 9208 php 9247 phpOLD 9259 fin1a2lem13 10452 axcclem 10497 isercolllem3 15703 mvdco 19463 dprdres 20048 dpjidcl 20078 ablfac1eulem 20092 cntzsdrg 20803 lspsnat 21147 lbsextlem2 21161 lbsextlem3 21162 cnsubdrglem 21436 mplmonmul 22054 clsconn 23438 2ndcdisj2 23465 kqdisj 23740 nulmbl2 25571 i1f1 25725 itg11 25726 itg1climres 25749 limcresi 25920 dvreslem 25944 dvres2lem 25945 dvaddbr 25974 dvmulbr 25975 dvmulbrOLD 25976 lhop 26055 elqaa 26364 difres 32613 imadifxp 32614 xrge00 33017 elrspunidl 33456 eulerpartlemmf 34377 eulerpartlemgf 34381 bj-2upln1upl 37025 pibt2 37418 mblfinlem3 37666 mblfinlem4 37667 ismblfin 37668 cnambfre 37675 divrngidl 38035 dvrelog2 42065 dvrelog3 42066 readvrec2 42391 readvrec 42392 dffltz 42644 cantnftermord 43333 omabs2 43345 radcnvrat 44333 fourierdlem62 46183 |
| Copyright terms: Public domain | W3C validator |