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 5984

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 5721	. . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
2	1	ineq2i 4163	. . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3		indi 4230	. . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
4	2, 3	eqtri 2784	. 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5		df-res 5663	. 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V))
6		df-res 5663	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
7		df-res 5663	. . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
8	6, 7	uneq12i 4113	. 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
9	4, 5, 8	3eqtr4i 2794	1 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1570 Vcvv 3451 ∪ cun 3897 ∩ cin 3898 × cxp 5649 ↾ cres 5653

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2733

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2740 df-cleq 2753 df-clel 2836 df-rab 3414 df-v 3453 df-un 3904 df-in 3906 df-opab 5168 df-xp 5657 df-res 5663

This theorem is used by: reldmun 6023 reldisjunOLD 6024 imaundi 6141 imadifssranOLD 6202 imadifssranOLDOLD 6203 relresfldOLD 6279 resasplit 6752 fresaunres2 6754 residpr 7146 fnsnsplit 7189 eqfunresadj 7370 tfrlem16 8401 mapunen 9165 fnfi 9193 fseq1p1m1 13732 resunimafz0 14590 gsum2dlem2 20185 dprd2da 20258 evlseu 22392 ptuncnv 24126 mbfres2 25966 nosupbnd2lem1 28072 noinfbnd2lem1 28087 ffsrn 33320 resf1o 33322 symgcom 33644 tocyc01 33679 cvmliftlem10 36059 poimirlem9 38547 disjresundif 39178 dvun 43410 eldioph4b 43817 pwssplit4 44090 tfsconcatrev 44349 undmrnresiss 44603 relexp0a 44715 rnresun 46194 tposresg 49985