| 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 4284 | . 2 ⊢ (𝐶 ∩ (𝐴 ∪ 𝐵)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) | |
| 2 | incom 4209 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = (𝐶 ∩ (𝐴 ∪ 𝐵)) | |
| 3 | incom 4209 | . . 3 ⊢ (𝐴 ∩ 𝐶) = (𝐶 ∩ 𝐴) | |
| 4 | incom 4209 | . . 3 ⊢ (𝐵 ∩ 𝐶) = (𝐶 ∩ 𝐵) | |
| 5 | 3, 4 | uneq12i 4166 | . 2 ⊢ ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) = ((𝐶 ∩ 𝐴) ∪ (𝐶 ∩ 𝐵)) |
| 6 | 1, 2, 5 | 3eqtr4i 2775 | 1 ⊢ ((𝐴 ∪ 𝐵) ∩ 𝐶) = ((𝐴 ∩ 𝐶) ∪ (𝐵 ∩ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∪ 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-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-un 3956 df-in 3958 |
| This theorem is referenced by: difundir 4291 undisj1 4462 disjpr2 4713 resundir 6012 predun 6349 djuassen 10219 fin23lem26 10365 fpwwe2lem12 10682 neitr 23188 fiuncmp 23412 connsuba 23428 trfil2 23895 tsmsres 24152 trust 24238 restmetu 24583 volun 25580 uniioombllem3 25620 itgsplitioo 25873 ppiprm 27194 chtprm 27196 chtdif 27201 ppidif 27206 cycpmco2f1 33144 carsgclctunlem1 34319 ballotlemfp1 34494 ballotlemgun 34527 mrsubvrs 35527 mthmpps 35587 fixun 35910 mbfposadd 37674 metakunt17 42222 metakunt21 42226 metakunt22 42227 metakunt24 42229 iunrelexp0 43715 31prm 47584 |
| Copyright terms: Public domain | W3C validator |