![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > indir | Structured version Visualization version GIF version |
Description: Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.) |
Ref | Expression |
---|---|
indir | ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indi 3906 | . 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) | |
2 | incom 3838 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵)) | |
3 | incom 3838 | . . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴) | |
4 | incom 3838 | . . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵) | |
5 | 3, 4 | uneq12i 3798 | . 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) |
6 | 1, 2, 5 | 3eqtr4i 2683 | 1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∪ cun 3605 ∩ cin 3606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-un 3612 df-in 3614 |
This theorem is referenced by: difundir 3913 undisj1 4062 disjpr2 4280 disjpr2OLD 4281 resundir 5446 predun 5742 cdaassen 9042 fin23lem26 9185 fpwwe2lem13 9502 neitr 21032 fiuncmp 21255 connsuba 21271 trfil2 21738 tsmsres 21994 trust 22080 restmetu 22422 volun 23359 uniioombllem3 23399 itgsplitioo 23649 ppiprm 24922 chtprm 24924 chtdif 24929 ppidif 24934 carsgclctunlem1 30507 ballotlemfp1 30681 ballotlemgun 30714 mrsubvrs 31545 mthmpps 31605 fixun 32141 mbfposadd 33587 iunrelexp0 38311 31prm 41837 |
Copyright terms: Public domain | W3C validator |