| 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 4472). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.) |
| Ref | Expression |
|---|---|
| undif1 | ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | undir 4287 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) | |
| 2 | invdif 4279 | . . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵) | |
| 3 | 2 | uneq1i 4164 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵) |
| 4 | uncom 4158 | . . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵)) | |
| 5 | unvdif 4475 | . . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V | |
| 6 | 4, 5 | eqtri 2765 | . . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V |
| 7 | 6 | ineq2i 4217 | . . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V) |
| 8 | inv1 4398 | . . 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 1540 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ∩ cin 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 |
| This theorem is referenced by: undif2 4477 undifr 4483 unidif0 5360 sofld 6207 fresaun 6779 ralxpmap 8936 enp1ilem 9312 difinf 9349 pwfilem 9356 infdif 10248 fin23lem11 10357 fin1a2lem13 10452 axcclem 10497 ttukeylem1 10549 ttukeylem7 10555 fpwwe2lem12 10682 hashbclem 14491 incexclem 15872 ramub1lem1 17064 ramub1lem2 17065 isstruct2 17186 setsdm 17207 mrieqvlemd 17672 mreexmrid 17686 islbs3 21157 lbsextlem4 21163 basdif0 22960 bwth 23418 locfincmp 23534 cldsubg 24119 nulmbl2 25571 volinun 25581 limcdif 25911 ellimc2 25912 limcmpt2 25919 dvreslem 25944 dvaddbr 25974 dvmulbr 25975 dvmulbrOLD 25976 lhop 26055 plyeq0 26250 rlimcnp 27008 difeq 32537 ffsrn 32740 symgcom2 33104 esumpad2 34057 measunl 34217 subfacp1lem1 35184 cvmscld 35278 pibt2 37418 stoweidlem44 46059 |
| Copyright terms: Public domain | W3C validator |