![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difun2 | Structured version Visualization version GIF version |
Description: Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
difun2 | ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difundir 4139 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) | |
2 | difid 4211 | . . 3 ⊢ (𝐵 ∖ 𝐵) = ∅ | |
3 | 2 | uneq2i 4020 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅) |
4 | un0 4225 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵) | |
5 | 1, 3, 4 | 3eqtri 2801 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1508 ∖ cdif 3821 ∪ cun 3822 ∅c0 4173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rab 3092 df-v 3412 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 |
This theorem is referenced by: uneqdifeq 4316 difprsn1 4604 orddif 6120 domunsncan 8412 elfiun 8688 hartogslem1 8800 cantnfp1lem3 8936 dju1dif 9395 infdju1 9412 ssxr 10509 dfn2 11721 incexclem 15050 mreexmrid 16785 lbsextlem4 19668 ufprim 22237 volun 23865 i1f1 24010 itgioo 24135 itgsplitioo 24157 plyeq0lem 24519 jensen 25284 difeq 30072 fzdif2 30289 fzodif2 30290 measun 31148 carsgclctunlem1 31253 carsggect 31254 chtvalz 31581 elmrsubrn 32320 mrsubvrs 32322 pibt2 34172 finixpnum 34351 lindsadd 34359 lindsenlbs 34361 poimirlem2 34368 poimirlem4 34370 poimirlem6 34372 poimirlem7 34373 poimirlem8 34374 poimirlem11 34377 poimirlem12 34378 poimirlem13 34379 poimirlem14 34380 poimirlem16 34382 poimirlem18 34384 poimirlem19 34385 poimirlem21 34387 poimirlem23 34389 poimirlem27 34393 poimirlem30 34396 asindmre 34451 kelac2 39095 pwfi2f1o 39126 iccdifioo 41252 iccdifprioo 41253 hoiprodp1 42331 |
Copyright terms: Public domain | W3C validator |