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 3958 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
2 | 1 | anim1d 610 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))) |
3 | eldif 3943 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶)) | |
4 | eldif 3943 | . . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)) | |
5 | 2, 3, 4 | 3imtr4g 297 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶))) |
6 | 5 | ssrdv 3970 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2105 ∖ cdif 3930 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-dif 3936 df-in 3940 df-ss 3949 |
This theorem is referenced by: ssdifd 4114 php 8689 pssnn 8724 fin1a2lem13 9822 axcclem 9867 isercolllem3 15011 mvdco 18502 dprdres 19079 dpjidcl 19109 ablfac1eulem 19123 cntzsdrg 19510 lspsnat 19846 lbsextlem2 19860 lbsextlem3 19861 mplmonmul 20173 cnsubdrglem 20524 clsconn 21966 2ndcdisj2 21993 kqdisj 22268 nulmbl2 24064 i1f1 24218 itg11 24219 itg1climres 24242 limcresi 24410 dvreslem 24434 dvres2lem 24435 dvaddbr 24462 dvmulbr 24463 lhop 24540 elqaa 24838 difres 30278 imadifxp 30279 xrge00 30600 eulerpartlemmf 31532 eulerpartlemgf 31536 bj-2upln1upl 34233 pibt2 34580 mblfinlem3 34812 mblfinlem4 34813 ismblfin 34814 cnambfre 34821 divrngidl 35187 dffltz 39149 radcnvrat 40523 fourierdlem62 42330 |
Copyright terms: Public domain | W3C validator |