![]() |
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 4200 | . 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) | |
2 | incom 4128 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵)) | |
3 | incom 4128 | . . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴) | |
4 | incom 4128 | . . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵) | |
5 | 3, 4 | uneq12i 4088 | . 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) |
6 | 1, 2, 5 | 3eqtr4i 2831 | 1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 ∪ cun 3879 ∩ cin 3880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-un 3886 df-in 3888 |
This theorem is referenced by: difundir 4207 undisj1 4369 disjpr2 4609 resundir 5833 predun 6140 djuassen 9589 fin23lem26 9736 fpwwe2lem13 10053 neitr 21785 fiuncmp 22009 connsuba 22025 trfil2 22492 tsmsres 22749 trust 22835 restmetu 23177 volun 24149 uniioombllem3 24189 itgsplitioo 24441 ppiprm 25736 chtprm 25738 chtdif 25743 ppidif 25748 cycpmco2f1 30816 carsgclctunlem1 31685 ballotlemfp1 31859 ballotlemgun 31892 mrsubvrs 32882 mthmpps 32942 fixun 33483 mbfposadd 35104 metakunt17 39366 metakunt21 39370 metakunt22 39371 metakunt24 39373 iunrelexp0 40403 31prm 44114 |
Copyright terms: Public domain | W3C validator |