Theorem resundir 5954

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

Syntax hints:   = wceq 1542  Vcvv 3430   ∪ cun 3888   ∩ cin 3889   × cxp 5623   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-in 3897  df-res 5637

This theorem is referenced by:  relresdm1  5993  imaundir  6109  fresaunres2  6707  fvunsn  7128  fvsnun1  7131  fvsnun2  7132  fsnunfv  7136  fsnunres  7137  frrlem12  8241  domss2  9068  axdc3lem4  10369  fseq1p1m1  13546  hashgval  14289  hashinf  14291  setsres  17142  setscom  17144  setsid  17171  pwssplit1  21049  nosupbnd2lem1  27696  noinfbnd2lem1  27711  noetasuplem2  27715  noetasuplem3  27716  noetasuplem4  27717  noetainflem2  27719  ex-res  30529  padct  32809  eulerpartlemt  34534  poimirlem3  37961  ecunres  38732  mapfzcons1  43166  diophrw  43208  eldioph2lem1  43209  eldioph2lem2  43210  diophin  43221  pwssplit4  43538