![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difundir | Structured version Visualization version GIF version |
Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004.) |
Ref | Expression |
---|---|
difundir | ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indir 4274 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) | |
2 | invdif 4267 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶) | |
3 | invdif 4267 | . . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶) | |
4 | invdif 4267 | . . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶) | |
5 | 3, 4 | uneq12i 4158 | . 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) |
6 | 1, 2, 5 | 3eqtr3i 2762 | 1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 Vcvv 3462 ∖ cdif 3943 ∪ cun 3944 ∩ cin 3945 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3949 df-un 3951 df-in 3953 |
This theorem is referenced by: dfsymdif3 4295 difun2 4475 diftpsn3 4801 strleun 17154 setsfun0 17169 mreexmrid 17651 mreexexlem2d 17653 mvdco 19439 dprd2da 20038 dmdprdsplit2lem 20041 ablfac1eulem 20068 lbsextlem4 21138 opsrtoslem2 22065 nulmbl2 25553 uniioombllem3 25602 sltlpss 27927 slelss 27928 ex-dif 30353 indifundif 32452 imadifxp 32521 fzodif1 32698 cycpmrn 33025 ballotlemfp1 34338 ballotlemgun 34371 onint1 36174 lindsadd 37327 lindsenlbs 37329 poimirlem2 37336 poimirlem6 37340 poimirlem7 37341 poimirlem8 37342 poimirlem22 37356 dvmptfprodlem 45601 fourierdlem102 45865 fourierdlem114 45877 caragenuncllem 46169 carageniuncllem1 46178 |
Copyright terms: Public domain | W3C validator |