![]() |
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 5206 | . . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V)) | |
2 | 1 | ineq2i 3844 | . . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) |
3 | indi 3906 | . . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) | |
4 | 2, 3 | eqtri 2673 | . 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) |
5 | df-res 5155 | . 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) | |
6 | df-res 5155 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
7 | df-res 5155 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
8 | 6, 7 | uneq12i 3798 | . 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) |
9 | 4, 5, 8 | 3eqtr4i 2683 | 1 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 Vcvv 3231 ∪ cun 3605 ∩ cin 3606 × cxp 5141 ↾ cres 5145 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-un 3612 df-in 3614 df-opab 4746 df-xp 5149 df-res 5155 |
This theorem is referenced by: imaundi 5580 relresfld 5700 resasplit 6112 fresaunres2 6114 residpr 6449 fnsnsplit 6491 tfrlem16 7534 mapunen 8170 fnfi 8279 fseq1p1m1 12452 resunimafz0 13267 gsum2dlem2 18416 dprd2da 18487 evlseu 19564 ptuncnv 21658 mbfres2 23457 ffsrn 29632 resf1o 29633 cvmliftlem10 31402 eqfunresadj 31785 nosupbnd2lem1 31986 poimirlem9 33548 eldioph4b 37692 pwssplit4 37976 undmrnresiss 38227 relexp0a 38325 rnresun 39676 |
Copyright terms: Public domain | W3C validator |