Theorem resundir 6014

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

Syntax hints:   = wceq 1536  Vcvv 3477   ∪ cun 3960   ∩ cin 3961   × cxp 5686   ↾ cres 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-un 3967  df-in 3969  df-res 5700

This theorem is referenced by:  relresdm1  6052  imaundir  6172  fresaunres2  6780  fvunsn  7198  fvsnun1  7201  fvsnun2  7202  fsnunfv  7206  fsnunres  7207  frrlem12  8320  wfrlem14OLD  8360  domss2  9174  axdc3lem4  10490  fseq1p1m1  13634  hashgval  14368  hashinf  14370  setsres  17211  setscom  17213  setsid  17241  pwssplit1  21075  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetasuplem2  27793  noetasuplem3  27794  noetasuplem4  27795  noetainflem2  27797  ex-res  30469  padct  32736  eulerpartlemt  34352  poimirlem3  37609  mapfzcons1  42704  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  diophin  42759  pwssplit4  43077