![]() |
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 4277 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5694 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
3 | df-res 5694 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
4 | df-res 5694 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
5 | 3, 4 | uneq12i 4161 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
6 | 1, 2, 5 | 3eqtr4i 2764 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 Vcvv 3462 ∪ cun 3945 ∩ cin 3946 × cxp 5680 ↾ cres 5684 |
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 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-un 3952 df-in 3954 df-res 5694 |
This theorem is referenced by: relresdm1 6042 imaundir 6162 fresaunres2 6774 fvunsn 7193 fvsnun1 7196 fvsnun2 7197 fsnunfv 7201 fsnunres 7202 frrlem12 8312 wfrlem14OLD 8352 domss2 9174 axdc3lem4 10496 fseq1p1m1 13629 hashgval 14350 hashinf 14352 setsres 17180 setscom 17182 setsid 17210 pwssplit1 21037 nosupbnd2lem1 27745 noinfbnd2lem1 27760 noetasuplem2 27764 noetasuplem3 27765 noetasuplem4 27766 noetainflem2 27768 ex-res 30374 padct 32633 eulerpartlemt 34205 poimirlem3 37324 mapfzcons1 42374 diophrw 42416 eldioph2lem1 42417 eldioph2lem2 42418 diophin 42429 pwssplit4 42750 |
Copyright terms: Public domain | W3C validator |