Theorem resundir 5980

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 5659	. 2 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ∪ 𝐵) ∩ (𝐶 × V))
3		df-res 5659	. . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
4		df-res 5659	. . 3 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
5	3, 4	uneq12i 4119	. 2 ⊢ ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
6	1, 2, 5	3eqtr4i 2795	1 ⊢ ((𝐴 ∪ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐶) ∪ (𝐵 ↾ 𝐶))

Syntax hints:   = wceq 1560  Vcvv 3454   ∪ cun 3902   ∩ cin 3903   × cxp 5645   ↾ cres 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-un 3909  df-in 3911  df-res 5659

This theorem is referenced by:  relresdm1  6022  imaundir  6135  fresaunres2  6736  fvunsn  7163  fvsnun1  7166  fvsnun2  7167  fsnunfv  7171  fsnunres  7172  frrlem12  8278  domss2  9108  axdc3lem4  10410  fseq1p1m1  13603  hashgval  14346  hashinf  14348  setsres  17214  setscom  17216  setsid  17243  pwssplit1  21126  nosupbnd2lem1  27779  noinfbnd2lem1  27794  noetasuplem2  27798  noetasuplem3  27799  noetasuplem4  27800  noetainflem2  27802  ex-res  30643  padct  32920  eulerpartlemt  34668  poimirlem3  38122  ecunres  38893  mapfzcons1  43298  diophrw  43340  eldioph2lem1  43341  eldioph2lem2  43342  diophin  43353  pwssplit4  43666