![]() |
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 3883 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 610 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))) |
3 | eldif 3869 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)) | |
4 | eldif 3869 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3imtr4g 297 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶))) |
6 | 5 | ssrdv 3895 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2081 ∖ cdif 3856 ⊆ wss 3859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-v 3439 df-dif 3862 df-in 3866 df-ss 3874 |
This theorem is referenced by: ssdifd 4038 php 8548 pssnn 8582 fin1a2lem13 9680 axcclem 9725 isercolllem3 14857 mvdco 18304 dprdres 18867 dpjidcl 18897 ablfac1eulem 18911 cntzsdrg 19271 lspsnat 19607 lbsextlem2 19621 lbsextlem3 19622 mplmonmul 19932 cnsubdrglem 20278 clsconn 21722 2ndcdisj2 21749 kqdisj 22024 nulmbl2 23820 i1f1 23974 itg11 23975 itg1climres 23998 limcresi 24166 dvreslem 24190 dvres2lem 24191 dvaddbr 24218 dvmulbr 24219 lhop 24296 elqaa 24594 difres 30040 imadifxp 30041 xrge00 30347 eulerpartlemmf 31250 eulerpartlemgf 31254 bj-2upln1upl 33960 pibt2 34248 mblfinlem3 34481 mblfinlem4 34482 ismblfin 34483 cnambfre 34490 divrngidl 34857 dffltz 38787 radcnvrat 40203 fourierdlem62 42015 |
Copyright terms: Public domain | W3C validator |