Theorem resundir 5953

Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)

Assertion

Ref	Expression
resundir	⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶))

Proof of Theorem resundir

Step	Hyp	Ref	Expression
1		indir 4238	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2		df-res 5636	. 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V))
3		df-res 5636	. . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
4		df-res 5636	. . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
5	3, 4	uneq12i 4118	. 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
6	1, 2, 5	3eqtr4i 2769	1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶))

Syntax hints:   = wceq 1541  Vcvv 3440   ∪ cun 3899   ∩ cin 3900   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-in 3908  df-res 5636

This theorem is referenced by:  relresdm1  5992  imaundir  6108  fresaunres2  6706  fvunsn  7125  fvsnun1  7128  fvsnun2  7129  fsnunfv  7133  fsnunres  7134  frrlem12  8239  domss2  9064  axdc3lem4  10363  fseq1p1m1  13514  hashgval  14256  hashinf  14258  setsres  17105  setscom  17107  setsid  17134  pwssplit1  21011  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetasuplem2  27702  noetasuplem3  27703  noetasuplem4  27704  noetainflem2  27706  ex-res  30516  padct  32797  eulerpartlemt  34528  poimirlem3  37824  ecunres  38589  mapfzcons1  42969  diophrw  43011  eldioph2lem1  43012  eldioph2lem2  43013  diophin  43024  pwssplit4  43341