![]() |
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 4134 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5412 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
3 | df-res 5412 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
4 | df-res 5412 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
5 | 3, 4 | uneq12i 4022 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
6 | 1, 2, 5 | 3eqtr4i 2806 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 Vcvv 3409 ∪ cun 3823 ∩ cin 3824 × cxp 5398 ↾ cres 5402 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-v 3411 df-un 3830 df-in 3832 df-res 5412 |
This theorem is referenced by: imaundir 5843 fresaunres2 6373 fvunsn 6758 fvsnun1 6763 fvsnun2 6764 fvsnun1OLD 6765 fvsnun2OLD 6766 fsnunfv 6770 fsnunres 6771 wfrlem14 7765 domss2 8464 axdc3lem4 9665 fseq1p1m1 12790 hashgval 13501 hashinf 13503 setsres 16371 setscom 16373 setsid 16384 pwssplit1 19543 ex-res 27988 funresdm1 30109 padct 30196 eulerpartlemt 31231 frrlem12 32595 nosupbnd2lem1 32676 noetalem2 32679 noetalem3 32680 poimirlem3 34284 mapfzcons1 38654 diophrw 38696 eldioph2lem1 38697 eldioph2lem2 38698 diophin 38710 pwssplit4 39030 |
Copyright terms: Public domain | W3C validator |