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 4195 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) | |
2 | difid 4285 | . . 3 ⊢ (𝐵 ∖ 𝐵) = ∅ | |
3 | 2 | uneq2i 4074 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ (𝐵 ∖ 𝐵)) = ((𝐴 ∖ 𝐵) ∪ ∅) |
4 | un0 4305 | . 2 ⊢ ((𝐴 ∖ 𝐵) ∪ ∅) = (𝐴 ∖ 𝐵) | |
5 | 1, 3, 4 | 3eqtri 2769 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐵) = (𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∖ cdif 3863 ∪ cun 3864 ∅c0 4237 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-nul 4238 |
This theorem is referenced by: uneqdifeq 4404 difprsn1 4713 orddif 6306 domunsncan 8745 elfiun 9046 hartogslem1 9158 cantnfp1lem3 9295 dju1dif 9786 infdju1 9803 ssxr 10902 dfn2 12103 incexclem 15400 mreexmrid 17146 lbsextlem4 20198 ufprim 22806 volun 24442 i1f1 24587 itgioo 24713 itgsplitioo 24735 plyeq0lem 25104 jensen 25871 difeq 30584 undif5 30586 fzdif2 30832 fzodif2 30833 pmtrcnel2 31078 measun 31891 carsgclctunlem1 31996 carsggect 31997 chtvalz 32321 elmrsubrn 33195 mrsubvrs 33197 pibt2 35325 finixpnum 35499 lindsadd 35507 lindsenlbs 35509 poimirlem2 35516 poimirlem4 35518 poimirlem6 35520 poimirlem7 35521 poimirlem8 35522 poimirlem11 35525 poimirlem12 35526 poimirlem13 35527 poimirlem14 35528 poimirlem16 35530 poimirlem18 35532 poimirlem19 35533 poimirlem21 35535 poimirlem23 35537 poimirlem27 35541 poimirlem30 35544 asindmre 35597 kelac2 40593 pwfi2f1o 40624 iccdifioo 42728 iccdifprioo 42729 hoiprodp1 43801 |
Copyright terms: Public domain | W3C validator |