| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > resundir | Structured version Visualization version GIF version | ||
| Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.) |
| Ref | Expression |
|---|---|
| resundir | ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | indir 4266 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
| 2 | df-res 5677 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
| 3 | df-res 5677 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
| 4 | df-res 5677 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
| 5 | 3, 4 | uneq12i 4146 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
| 6 | 1, 2, 5 | 3eqtr4i 2767 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1539 Vcvv 3463 ∪ cun 3929 ∩ cin 3930 × cxp 5663 ↾ cres 5667 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2706 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2713 df-cleq 2726 df-clel 2808 df-rab 3420 df-v 3465 df-un 3936 df-in 3938 df-res 5677 |
| This theorem is referenced by: relresdm1 6031 imaundir 6150 fresaunres2 6760 fvunsn 7181 fvsnun1 7184 fvsnun2 7185 fsnunfv 7189 fsnunres 7190 frrlem12 8304 wfrlem14OLD 8344 domss2 9158 axdc3lem4 10475 fseq1p1m1 13620 hashgval 14354 hashinf 14356 setsres 17197 setscom 17199 setsid 17226 pwssplit1 21026 nosupbnd2lem1 27696 noinfbnd2lem1 27711 noetasuplem2 27715 noetasuplem3 27716 noetasuplem4 27717 noetainflem2 27719 ex-res 30388 padct 32666 eulerpartlemt 34332 poimirlem3 37589 mapfzcons1 42691 diophrw 42733 eldioph2lem1 42734 eldioph2lem2 42735 diophin 42746 pwssplit4 43064 |
| Copyright terms: Public domain | W3C validator |