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 3992). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
undif1 | ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | undir 3835 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) | |
2 | invdif 3827 | . . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | |
3 | 2 | uneq1i 3725 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵) |
4 | uncom 3719 | . . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵)) | |
5 | unvdif 3994 | . . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V | |
6 | 4, 5 | eqtri 2632 | . . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V |
7 | 6 | ineq2i 3773 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V) |
8 | inv1 3922 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵) | |
9 | 7, 8 | eqtri 2632 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵) |
10 | 1, 3, 9 | 3eqtr3i 2640 | 1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 |
This theorem is referenced by: undif2 3996 unidif0 4764 pwundif 4945 sofld 5500 fresaun 5988 ralxpmap 7793 enp1ilem 8079 difinf 8115 pwfilem 8143 infdif 8914 fin23lem11 9022 fin1a2lem13 9117 axcclem 9162 ttukeylem1 9214 ttukeylem7 9220 fpwwe2lem13 9343 hashbclem 13093 incexclem 14407 ramub1lem1 15568 ramub1lem2 15569 isstruct2 15704 setsdm 15724 mrieqvlemd 16112 mreexmrid 16126 islbs3 18976 lbsextlem4 18982 basdif0 20568 bwth 21023 locfincmp 21139 cldsubg 21724 nulmbl2 23111 volinun 23121 limcdif 23446 ellimc2 23447 limcmpt2 23454 dvreslem 23479 dvaddbr 23507 dvmulbr 23508 lhop 23583 plyeq0 23771 rlimcnp 24492 difeq 28739 ffsrn 28892 esumpad2 29445 measunl 29606 subfacp1lem1 30415 cvmscld 30509 compne 37665 stoweidlem44 38937 |
Copyright terms: Public domain | W3C validator |