![]() |
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 4282 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) | |
2 | difid 4375 | . . 3 ⊢ (𝐵 ∖ 𝐵) = ∅ | |
3 | 2 | uneq2i 4160 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅) |
4 | un0 4395 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵) | |
5 | 1, 3, 4 | 3eqtri 2758 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∖ cdif 3944 ∪ cun 3945 ∅c0 4325 |
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-or 846 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-in 3954 df-nul 4326 |
This theorem is referenced by: undif5 4489 uneqdifeq 4497 difprsn1 4809 orddif 6472 domunsncan 9110 elfiun 9473 hartogslem1 9585 cantnfp1lem3 9723 dju1dif 10215 infdju1 10232 ssxr 11333 dfn2 12537 incexclem 15840 mreexmrid 17656 lbsextlem4 21142 ufprim 23904 volun 25565 i1f1 25710 itgioo 25836 itgsplitioo 25858 plyeq0lem 26237 jensen 27017 difeq 32445 fzdif2 32693 fzodif2 32694 pmtrcnel2 32968 measun 34044 carsgclctunlem1 34151 carsggect 34152 chtvalz 34475 elmrsubrn 35348 mrsubvrs 35350 pibt2 37124 finixpnum 37306 lindsadd 37314 lindsenlbs 37316 poimirlem2 37323 poimirlem4 37325 poimirlem6 37327 poimirlem7 37328 poimirlem8 37329 poimirlem11 37332 poimirlem12 37333 poimirlem13 37334 poimirlem14 37335 poimirlem16 37337 poimirlem18 37339 poimirlem19 37340 poimirlem21 37342 poimirlem23 37344 poimirlem27 37348 poimirlem30 37351 asindmre 37404 disjresundif 37940 kelac2 42726 pwfi2f1o 42757 iccdifioo 45133 iccdifprioo 45134 hoiprodp1 46209 |
Copyright terms: Public domain | W3C validator |