![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > undif1 | Structured version Visualization version GIF version |
Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4436). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
undif1 | ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | undir 4241 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) | |
2 | invdif 4233 | . . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | |
3 | 2 | uneq1i 4124 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵) |
4 | uncom 4118 | . . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵)) | |
5 | unvdif 4439 | . . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V | |
6 | 4, 5 | eqtri 2765 | . . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V |
7 | 6 | ineq2i 4174 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V) |
8 | inv1 4359 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵) | |
9 | 7, 8 | eqtri 2765 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵) |
10 | 1, 3, 9 | 3eqtr3i 2773 | 1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 Vcvv 3448 ∖ cdif 3912 ∪ cun 3913 ∩ cin 3914 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 |
This theorem is referenced by: undif2 4441 unidif0 5320 sofld 6144 fresaun 6718 ralxpmap 8841 pwfilem 9128 enp1ilem 9229 difinf 9267 pwfilemOLD 9297 infdif 10152 fin23lem11 10260 fin1a2lem13 10355 axcclem 10400 ttukeylem1 10452 ttukeylem7 10458 fpwwe2lem12 10585 hashbclem 14356 incexclem 15728 ramub1lem1 16905 ramub1lem2 16906 isstruct2 17028 setsdm 17049 mrieqvlemd 17516 mreexmrid 17530 islbs3 20632 lbsextlem4 20638 basdif0 22319 bwth 22777 locfincmp 22893 cldsubg 23478 nulmbl2 24916 volinun 24926 limcdif 25256 ellimc2 25257 limcmpt2 25264 dvreslem 25289 dvaddbr 25318 dvmulbr 25319 lhop 25396 plyeq0 25588 rlimcnp 26331 difeq 31487 ffsrn 31688 symgcom2 31977 esumpad2 32695 measunl 32855 subfacp1lem1 33813 cvmscld 33907 pibt2 35917 stoweidlem44 44359 |
Copyright terms: Public domain | W3C validator |