![]() |
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 4276 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5689 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
3 | df-res 5689 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
4 | df-res 5689 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
5 | 3, 4 | uneq12i 4162 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
6 | 1, 2, 5 | 3eqtr4i 2771 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 Vcvv 3475 ∪ cun 3947 ∩ cin 3948 × cxp 5675 ↾ cres 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-un 3954 df-in 3956 df-res 5689 |
This theorem is referenced by: relresdm1 6034 imaundir 6151 fresaunres2 6764 fvunsn 7177 fvsnun1 7180 fvsnun2 7181 fsnunfv 7185 fsnunres 7186 frrlem12 8282 wfrlem14OLD 8322 domss2 9136 axdc3lem4 10448 fseq1p1m1 13575 hashgval 14293 hashinf 14295 setsres 17111 setscom 17113 setsid 17141 pwssplit1 20670 nosupbnd2lem1 27218 noinfbnd2lem1 27233 noetasuplem2 27237 noetasuplem3 27238 noetasuplem4 27239 noetainflem2 27241 ex-res 29694 padct 31944 eulerpartlemt 33370 poimirlem3 36491 mapfzcons1 41455 diophrw 41497 eldioph2lem1 41498 eldioph2lem2 41499 diophin 41510 pwssplit4 41831 |
Copyright terms: Public domain | W3C validator |