![]() |
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 4233 | . 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) | |
2 | df-res 5643 | . 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) | |
3 | df-res 5643 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
4 | df-res 5643 | . . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) | |
5 | 3, 4 | uneq12i 4119 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V))) |
6 | 1, 2, 5 | 3eqtr4i 2775 | 1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 Vcvv 3443 ∪ cun 3906 ∩ cin 3907 × cxp 5629 ↾ cres 5633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3406 df-v 3445 df-un 3913 df-in 3915 df-res 5643 |
This theorem is referenced by: imaundir 6101 fresaunres2 6711 fvunsn 7121 fvsnun1 7124 fvsnun2 7125 fsnunfv 7129 fsnunres 7130 frrlem12 8220 wfrlem14OLD 8260 domss2 9038 axdc3lem4 10347 fseq1p1m1 13469 hashgval 14187 hashinf 14189 setsres 17010 setscom 17012 setsid 17040 pwssplit1 20473 nosupbnd2lem1 27015 noinfbnd2lem1 27030 noetasuplem2 27034 noetasuplem3 27035 noetasuplem4 27036 noetainflem2 27038 ex-res 29214 funresdm1 31352 padct 31462 eulerpartlemt 32783 poimirlem3 36019 mapfzcons1 40949 diophrw 40991 eldioph2lem1 40992 eldioph2lem2 40993 diophin 41004 pwssplit4 41325 |
Copyright terms: Public domain | W3C validator |