| 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 4252 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
| 2 | df-res 5653 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
| 3 | df-res 5653 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
| 4 | df-res 5653 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
| 5 | 3, 4 | uneq12i 4132 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
| 6 | 1, 2, 5 | 3eqtr4i 2763 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 Vcvv 3450 ∪ cun 3915 ∩ cin 3916 × cxp 5639 ↾ cres 5643 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2702 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1543 df-ex 1780 df-sb 2066 df-clab 2709 df-cleq 2722 df-clel 2804 df-rab 3409 df-v 3452 df-un 3922 df-in 3924 df-res 5653 |
| This theorem is referenced by: relresdm1 6007 imaundir 6126 fresaunres2 6735 fvunsn 7156 fvsnun1 7159 fvsnun2 7160 fsnunfv 7164 fsnunres 7165 frrlem12 8279 domss2 9106 axdc3lem4 10413 fseq1p1m1 13566 hashgval 14305 hashinf 14307 setsres 17155 setscom 17157 setsid 17184 pwssplit1 20973 nosupbnd2lem1 27634 noinfbnd2lem1 27649 noetasuplem2 27653 noetasuplem3 27654 noetasuplem4 27655 noetainflem2 27657 ex-res 30377 padct 32650 eulerpartlemt 34369 poimirlem3 37624 mapfzcons1 42712 diophrw 42754 eldioph2lem1 42755 eldioph2lem2 42756 diophin 42767 pwssplit4 43085 |
| Copyright terms: Public domain | W3C validator |