Theorem resundir 5961

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

Syntax hints:   = wceq 1542  Vcvv 3442   ∪ cun 3901   ∩ cin 3902   × cxp 5630   ↾ cres 5634

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 3402  df-v 3444  df-un 3908  df-in 3910  df-res 5644

This theorem is referenced by:  relresdm1  6000  imaundir  6116  fresaunres2  6714  fvunsn  7135  fvsnun1  7138  fvsnun2  7139  fsnunfv  7143  fsnunres  7144  frrlem12  8249  domss2  9076  axdc3lem4  10375  fseq1p1m1  13526  hashgval  14268  hashinf  14270  setsres  17117  setscom  17119  setsid  17146  pwssplit1  21026  nosupbnd2lem1  27698  noinfbnd2lem1  27713  noetasuplem2  27717  noetasuplem3  27718  noetasuplem4  27719  noetainflem2  27721  ex-res  30532  padct  32812  eulerpartlemt  34553  poimirlem3  37878  ecunres  38649  mapfzcons1  43078  diophrw  43120  eldioph2lem1  43121  eldioph2lem2  43122  diophin  43133  pwssplit4  43450