![]() |
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 3938 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 612 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))) |
3 | eldif 3921 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)) | |
4 | eldif 3921 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3imtr4g 296 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶))) |
6 | 5 | ssrdv 3951 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∈ wcel 2107 ∖ cdif 3908 ⊆ wss 3911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-dif 3914 df-in 3918 df-ss 3928 |
This theorem is referenced by: ssdifd 4101 pssnn 9115 php 9157 phpOLD 9169 pssnnOLD 9212 fin1a2lem13 10353 axcclem 10398 isercolllem3 15557 mvdco 19232 dprdres 19812 dpjidcl 19842 ablfac1eulem 19856 cntzsdrg 20283 lspsnat 20622 lbsextlem2 20636 lbsextlem3 20637 cnsubdrglem 20864 mplmonmul 21453 clsconn 22797 2ndcdisj2 22824 kqdisj 23099 nulmbl2 24916 i1f1 25070 itg11 25071 itg1climres 25095 limcresi 25265 dvreslem 25289 dvres2lem 25290 dvaddbr 25318 dvmulbr 25319 lhop 25396 elqaa 25698 difres 31564 imadifxp 31565 xrge00 31926 elrspunidl 32251 eulerpartlemmf 33032 eulerpartlemgf 33036 bj-2upln1upl 35541 pibt2 35934 mblfinlem3 36163 mblfinlem4 36164 ismblfin 36165 cnambfre 36172 divrngidl 36533 dvrelog2 40567 dvrelog3 40568 dffltz 41015 cantnftermord 41698 omabs2 41710 radcnvrat 42682 fourierdlem62 44495 |
Copyright terms: Public domain | W3C validator |