Theorem resundi 5865

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 5618	. . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
2	1	ineq2i 4124	. . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3		indi 4188	. . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
4	2, 3	eqtri 2765	. 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5		df-res 5563	. 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V))
6		df-res 5563	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
7		df-res 5563	. . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
8	6, 7	uneq12i 4075	. 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
9	4, 5, 8	3eqtr4i 2775	1 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))

Syntax hints:   = wceq 1543  Vcvv 3408   ∪ cun 3864   ∩ cin 3865   × cxp 5549   ↾ cres 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-un 3871  df-in 3873  df-opab 5116  df-xp 5557  df-res 5563

This theorem is referenced by:  imaundi  6013  relresfld  6139  resasplit  6589  fresaunres2  6591  residpr  6958  fnsnsplit  6999  tfrlem16  8129  mapunen  8815  fnfi  8858  fseq1p1m1  13186  resunimafz0  14009  gsum2dlem2  19356  dprd2da  19429  evlseu  21043  ptuncnv  22704  mbfres2  24542  reldisjun  30661  ffsrn  30784  resf1o  30785  symgcom  31071  tocyc01  31104  cvmliftlem10  32969  eqfunresadj  33454  nosupbnd2lem1  33655  noinfbnd2lem1  33670  poimirlem9  35523  eldioph4b  40336  pwssplit4  40617  undmrnresiss  40888  relexp0a  41001  rnresun  42389