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 4250 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5560 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
3 | df-res 5560 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
4 | df-res 5560 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
5 | 3, 4 | uneq12i 4135 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
6 | 1, 2, 5 | 3eqtr4i 2852 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1531 Vcvv 3493 ∪ cun 3932 ∩ cin 3933 × cxp 5546 ↾ cres 5550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-rab 3145 df-v 3495 df-un 3939 df-in 3941 df-res 5560 |
This theorem is referenced by: imaundir 6002 fresaunres2 6543 fvunsn 6934 fvsnun1 6937 fvsnun2 6938 fsnunfv 6942 fsnunres 6943 wfrlem14 7960 domss2 8668 axdc3lem4 9867 fseq1p1m1 12973 hashgval 13685 hashinf 13687 setsres 16517 setscom 16519 setsid 16530 pwssplit1 19823 ex-res 28212 funresdm1 30347 padct 30447 eulerpartlemt 31622 frrlem12 33127 nosupbnd2lem1 33208 noetalem2 33211 noetalem3 33212 poimirlem3 34887 mapfzcons1 39305 diophrw 39347 eldioph2lem1 39348 eldioph2lem2 39349 diophin 39360 pwssplit4 39680 |
Copyright terms: Public domain | W3C validator |