Theorem resundir 5861

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

Syntax hints:   = wceq 1531  Vcvv 3493   ∪ cun 3932   ∩ cin 3933   × cxp 5546   ↾ cres 5550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-un 3939  df-in 3941  df-res 5560

This theorem is referenced by:  imaundir  6002  fresaunres2  6543  fvunsn  6934  fvsnun1  6937  fvsnun2  6938  fsnunfv  6942  fsnunres  6943  wfrlem14  7960  domss2  8668  axdc3lem4  9867  fseq1p1m1  12973  hashgval  13685  hashinf  13687  setsres  16517  setscom  16519  setsid  16530  pwssplit1  19823  ex-res  28212  funresdm1  30347  padct  30447  eulerpartlemt  31622  frrlem12  33127  nosupbnd2lem1  33208  noetalem2  33211  noetalem3  33212  poimirlem3  34887  mapfzcons1  39305  diophrw  39347  eldioph2lem1  39348  eldioph2lem2  39349  diophin  39360  pwssplit4  39680