resundi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > resundi		Structured version Visualization version GIF version

Theorem resundi 5988

Description: Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)

**Assertion**
Ref	Expression
resundi	⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))

**Proof of Theorem resundi**
Step	Hyp	Ref	Expression
1		xpundir 5724	. . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
2	1	ineq2i 4116	. . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3		indi 4231	. . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
4	2, 3	eqtri 2786	. 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5		df-res 5666	. 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V))
6		df-res 5666	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
7		df-res 5666	. . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
8	6, 7	uneq12i 4167	. 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
9	4, 5, 8	3eqtr4i 2796	1 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1569 Vcvv 3453 ∩ cin 4091 ∪ cun 4151 × cxp 5652 ↾ cres 5656

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-ext 2735

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-tru 1572 df-ex 1812 df-sb 2101 df-clab 2742 df-cleq 2755 df-clel 2838 df-rab 3416 df-v 3455 df-in 4093 df-un 4153 df-opab 5170 df-xp 5660 df-res 5666

This theorem is used by: reldmun 6028 reldisjunOLD 6029 imaundi 6146 imadifssranOLD 6208 imadifssranOLDOLD 6209 relresfldOLD 6285 resasplit 6760 fresaunres2 6762 residpr 7154 fnsnsplit 7196 eqfunresadj 7377 tfrlem16 8412 mapunen 9176 fnfi 9204 fseq1p1m1 13742 resunimafz0 14600 gsum2dlem2 20197 dprd2da 20270 evlseu 22404 ptuncnv 24138 mbfres2 25978 nosupbnd2lem1 28084 noinfbnd2lem1 28099 ffsrn 33373 resf1o 33375 symgcom 33697 tocyc01 33732 cvmliftlem10 36180 poimirlem9 38687 disjresundif 39318 dvun 43550 eldioph4b 43958 pwssplit4 44231 tfsconcatrev 44490 undmrnresiss 44744 relexp0a 44856 rnresun 46334 tposresg 50130