![]() |
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 4239 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) | |
2 | difid 4329 | . . 3 ⊢ (𝐵 ∖ 𝐵) = ∅ | |
3 | 2 | uneq2i 4119 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅) |
4 | un0 4349 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵) | |
5 | 1, 3, 4 | 3eqtri 2768 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∖ cdif 3906 ∪ cun 3907 ∅c0 4281 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-nul 4282 |
This theorem is referenced by: undif5 4441 uneqdifeq 4449 difprsn1 4759 orddif 6412 domunsncan 9013 elfiun 9363 hartogslem1 9475 cantnfp1lem3 9613 dju1dif 10105 infdju1 10122 ssxr 11221 dfn2 12423 incexclem 15718 mreexmrid 17520 lbsextlem4 20618 ufprim 23256 volun 24905 i1f1 25050 itgioo 25176 itgsplitioo 25198 plyeq0lem 25567 jensen 26334 difeq 31343 fzdif2 31589 fzodif2 31590 pmtrcnel2 31836 measun 32701 carsgclctunlem1 32808 carsggect 32809 chtvalz 33133 elmrsubrn 34005 mrsubvrs 34007 pibt2 35877 finixpnum 36052 lindsadd 36060 lindsenlbs 36062 poimirlem2 36069 poimirlem4 36071 poimirlem6 36073 poimirlem7 36074 poimirlem8 36075 poimirlem11 36078 poimirlem12 36079 poimirlem13 36080 poimirlem14 36081 poimirlem16 36083 poimirlem18 36085 poimirlem19 36086 poimirlem21 36088 poimirlem23 36090 poimirlem27 36094 poimirlem30 36097 asindmre 36150 disjresundif 36689 kelac2 41368 pwfi2f1o 41399 iccdifioo 43723 iccdifprioo 43724 hoiprodp1 44799 |
Copyright terms: Public domain | W3C validator |