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 6000

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 5728	. . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
2	1	ineq2i 4117	. . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3		indi 4232	. . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
4	2, 3	eqtri 2786	. 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5		df-res 5670	. 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V))
6		df-res 5670	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
7		df-res 5670	. . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
8	6, 7	uneq12i 4168	. 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
9	4, 5, 8	3eqtr4i 2796	1 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 Vcvv 3454 ∩ cin 4092 ∪ cun 4152 × cxp 5656 ↾ cres 5660

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-ext 2735

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-tru 1573 df-ex 1813 df-sb 2102 df-clab 2742 df-cleq 2755 df-clel 2839 df-rab 3417 df-v 3456 df-in 4094 df-un 4154 df-opab 5174 df-xp 5664 df-res 5670

This theorem is used by: reldmun 6041 reldisjunOLD 6042 imaundi 6159 imadifssranOLD 6221 imadifssranOLDOLD 6222 relresfldOLD 6303 resasplit 6782 fresaunres2 6784 residpr 7178 fnsnsplit 7220 eqfunresadj 7401 tfrlem16 8439 mapunen 9203 fnfi 9231 fseq1p1m1 13772 resunimafz0 14631 gsum2dlem2 20236 dprd2da 20309 evlseu 22447 ptuncnv 24181 mbfres2 26021 nosupbnd2lem1 28129 noinfbnd2lem1 28144 ffsrn 33416 resf1o 33418 symgcom 33743 tocyc01 33778 cvmliftlem10 36267 poimirlem9 38815 disjresundif 39444 dvun 43676 eldioph4b 44084 pwssplit4 44357 tfsconcatrev 44611 undmrnresiss 44865 relexp0a 44977 rnresun 46468 tposresg 50322