![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resundi | Structured version Visualization version GIF version |
Description: Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
Ref | Expression |
---|---|
resundi | ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpundir 5746 | . . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V)) | |
2 | 1 | ineq2i 4210 | . . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) |
3 | indi 4274 | . . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) | |
4 | 2, 3 | eqtri 2761 | . 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) |
5 | df-res 5689 | . 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) | |
6 | df-res 5689 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
7 | df-res 5689 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
8 | 6, 7 | uneq12i 4162 | . 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) |
9 | 4, 5, 8 | 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-opab 5212 df-xp 5683 df-res 5689 |
This theorem is referenced by: reldisjun 6033 imaundi 6150 relresfld 6276 resasplit 6762 fresaunres2 6764 residpr 7141 fnsnsplit 7182 eqfunresadj 7357 tfrlem16 8393 mapunen 9146 fnfi 9181 fseq1p1m1 13575 resunimafz0 14404 gsum2dlem2 19839 dprd2da 19912 evlseu 21646 ptuncnv 23311 mbfres2 25162 nosupbnd2lem1 27218 noinfbnd2lem1 27233 ffsrn 31954 resf1o 31955 symgcom 32244 tocyc01 32277 cvmliftlem10 34285 poimirlem9 36497 disjresundif 37109 eldioph4b 41549 pwssplit4 41831 tfsconcatrev 42098 undmrnresiss 42355 relexp0a 42467 rnresun 43876 |
Copyright terms: Public domain | W3C validator |