![]() |
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 4274 | . 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) | |
2 | incom 4202 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵)) | |
3 | incom 4202 | . . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴) | |
4 | incom 4202 | . . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵) | |
5 | 3, 4 | uneq12i 4162 | . 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) |
6 | 1, 2, 5 | 3eqtr4i 2771 | 1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∪ cun 3947 ∩ cin 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-un 3954 df-in 3956 |
This theorem is referenced by: difundir 4281 undisj1 4462 disjpr2 4718 resundir 5997 predun 6330 djuassen 10173 fin23lem26 10320 fpwwe2lem12 10637 neitr 22684 fiuncmp 22908 connsuba 22924 trfil2 23391 tsmsres 23648 trust 23734 restmetu 24079 volun 25062 uniioombllem3 25102 itgsplitioo 25355 ppiprm 26655 chtprm 26657 chtdif 26662 ppidif 26667 cycpmco2f1 32283 carsgclctunlem1 33316 ballotlemfp1 33490 ballotlemgun 33523 mrsubvrs 34513 mthmpps 34573 fixun 34881 mbfposadd 36535 metakunt17 41001 metakunt21 41005 metakunt22 41006 metakunt24 41008 iunrelexp0 42453 31prm 46265 |
Copyright terms: Public domain | W3C validator |