| 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 4286 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
| 2 | df-res 5697 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
| 3 | df-res 5697 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
| 4 | df-res 5697 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
| 5 | 3, 4 | uneq12i 4166 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
| 6 | 1, 2, 5 | 3eqtr4i 2775 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 Vcvv 3480 ∪ cun 3949 ∩ cin 3950 × cxp 5683 ↾ cres 5687 |
| 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 df-res 5697 |
| This theorem is referenced by: relresdm1 6051 imaundir 6170 fresaunres2 6780 fvunsn 7199 fvsnun1 7202 fvsnun2 7203 fsnunfv 7207 fsnunres 7208 frrlem12 8322 wfrlem14OLD 8362 domss2 9176 axdc3lem4 10493 fseq1p1m1 13638 hashgval 14372 hashinf 14374 setsres 17215 setscom 17217 setsid 17244 pwssplit1 21058 nosupbnd2lem1 27760 noinfbnd2lem1 27775 noetasuplem2 27779 noetasuplem3 27780 noetasuplem4 27781 noetainflem2 27783 ex-res 30460 padct 32731 eulerpartlemt 34373 poimirlem3 37630 mapfzcons1 42728 diophrw 42770 eldioph2lem1 42771 eldioph2lem2 42772 diophin 42783 pwssplit4 43101 |
| Copyright terms: Public domain | W3C validator |