Theorem resundir 6012

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

Syntax hints:   = wceq 1540  Vcvv 3480   ∪ cun 3949   ∩ cin 3950   × cxp 5683   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-in 3958  df-res 5697

This theorem is referenced by:  relresdm1  6051  imaundir  6170  fresaunres2  6780  fvunsn  7199  fvsnun1  7202  fvsnun2  7203  fsnunfv  7207  fsnunres  7208  frrlem12  8322  wfrlem14OLD  8362  domss2  9176  axdc3lem4  10493  fseq1p1m1  13638  hashgval  14372  hashinf  14374  setsres  17215  setscom  17217  setsid  17244  pwssplit1  21058  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem2  27779  noetasuplem3  27780  noetasuplem4  27781  noetainflem2  27783  ex-res  30460  padct  32731  eulerpartlemt  34373  poimirlem3  37630  mapfzcons1  42728  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  diophin  42783  pwssplit4  43101