![]() |
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 5744 | . . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V)) | |
2 | 1 | ineq2i 4208 | . . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) |
3 | indi 4272 | . . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) | |
4 | 2, 3 | eqtri 2758 | . 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) |
5 | df-res 5687 | . 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) | |
6 | df-res 5687 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
7 | df-res 5687 | . . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V)) | |
8 | 6, 7 | uneq12i 4160 | . 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V))) |
9 | 4, 5, 8 | 3eqtr4i 2768 | 1 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 Vcvv 3472 ∪ cun 3945 ∩ cin 3946 × cxp 5673 ↾ cres 5677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rab 3431 df-v 3474 df-un 3952 df-in 3954 df-opab 5210 df-xp 5681 df-res 5687 |
This theorem is referenced by: reldisjun 6031 imaundi 6148 relresfld 6274 resasplit 6760 fresaunres2 6762 residpr 7142 fnsnsplit 7183 eqfunresadj 7359 tfrlem16 8395 mapunen 9148 fnfi 9183 fseq1p1m1 13579 resunimafz0 14408 gsum2dlem2 19880 dprd2da 19953 evlseu 21865 ptuncnv 23531 mbfres2 25394 nosupbnd2lem1 27454 noinfbnd2lem1 27469 ffsrn 32221 resf1o 32222 symgcom 32514 tocyc01 32547 cvmliftlem10 34583 poimirlem9 36800 disjresundif 37412 eldioph4b 41851 pwssplit4 42133 tfsconcatrev 42400 undmrnresiss 42657 relexp0a 42769 rnresun 44177 |
Copyright terms: Public domain | W3C validator |