Theorem resundir 5965

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

Syntax hints:   = wceq 1540  Vcvv 3447   ∪ cun 3912   ∩ cin 3913   × cxp 5636   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-in 3921  df-res 5650

This theorem is referenced by:  relresdm1  6004  imaundir  6123  fresaunres2  6732  fvunsn  7153  fvsnun1  7156  fvsnun2  7157  fsnunfv  7161  fsnunres  7162  frrlem12  8276  domss2  9100  axdc3lem4  10406  fseq1p1m1  13559  hashgval  14298  hashinf  14300  setsres  17148  setscom  17150  setsid  17177  pwssplit1  20966  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem2  27646  noetasuplem3  27647  noetasuplem4  27648  noetainflem2  27650  ex-res  30370  padct  32643  eulerpartlemt  34362  poimirlem3  37617  mapfzcons1  42705  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  diophin  42760  pwssplit4  43078