![]() |
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 3973 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 609 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))) |
3 | eldif 3957 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)) | |
4 | eldif 3957 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3imtr4g 295 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶))) |
6 | 5 | ssrdv 3985 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 ∈ wcel 2099 ∖ cdif 3944 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-dif 3950 df-ss 3964 |
This theorem is referenced by: ssdifd 4140 pssnn 9206 php 9244 phpOLD 9256 pssnnOLD 9299 fin1a2lem13 10455 axcclem 10500 isercolllem3 15671 mvdco 19443 dprdres 20028 dpjidcl 20058 ablfac1eulem 20072 cntzsdrg 20781 lspsnat 21126 lbsextlem2 21140 lbsextlem3 21141 cnsubdrglem 21415 mplmonmul 22043 clsconn 23425 2ndcdisj2 23452 kqdisj 23727 nulmbl2 25556 i1f1 25710 itg11 25711 itg1climres 25735 limcresi 25905 dvreslem 25929 dvres2lem 25930 dvaddbr 25959 dvmulbr 25960 dvmulbrOLD 25961 lhop 26040 elqaa 26350 difres 32520 imadifxp 32521 xrge00 32895 elrspunidl 33303 eulerpartlemmf 34209 eulerpartlemgf 34213 bj-2upln1upl 36731 pibt2 37124 mblfinlem3 37360 mblfinlem4 37361 ismblfin 37362 cnambfre 37369 divrngidl 37729 dvrelog2 41763 dvrelog3 41764 dffltz 42288 cantnftermord 42986 omabs2 42998 radcnvrat 43988 fourierdlem62 45789 |
Copyright terms: Public domain | W3C validator |