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 4386). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
undif1 | ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | undir 4191 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) | |
2 | invdif 4183 | . . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | |
3 | 2 | uneq1i 4073 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵) |
4 | uncom 4067 | . . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵)) | |
5 | unvdif 4389 | . . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V | |
6 | 4, 5 | eqtri 2765 | . . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V |
7 | 6 | ineq2i 4124 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V) |
8 | inv1 4309 | . . 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 1543 Vcvv 3408 ∖ cdif 3863 ∪ cun 3864 ∩ cin 3865 |
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-ss 3883 df-nul 4238 |
This theorem is referenced by: undif2 4391 unidif0 5251 pwundifOLD 5452 sofld 6050 fresaun 6590 ralxpmap 8577 pwfilem 8855 enp1ilem 8908 difinf 8941 pwfilemOLD 8970 infdif 9823 fin23lem11 9931 fin1a2lem13 10026 axcclem 10071 ttukeylem1 10123 ttukeylem7 10129 fpwwe2lem12 10256 hashbclem 14016 incexclem 15400 ramub1lem1 16579 ramub1lem2 16580 isstruct2 16702 setsdm 16723 mrieqvlemd 17132 mreexmrid 17146 islbs3 20192 lbsextlem4 20198 basdif0 21850 bwth 22307 locfincmp 22423 cldsubg 23008 nulmbl2 24433 volinun 24443 limcdif 24773 ellimc2 24774 limcmpt2 24781 dvreslem 24806 dvaddbr 24835 dvmulbr 24836 lhop 24913 plyeq0 25105 rlimcnp 25848 difeq 30584 ffsrn 30784 symgcom2 31072 esumpad2 31736 measunl 31896 subfacp1lem1 32854 cvmscld 32948 pibt2 35325 stoweidlem44 43260 |
Copyright terms: Public domain | W3C validator |