Theorem resundir 5993

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

Syntax hints:   = wceq 1570  Vcvv 3455   ∪ cun 3903   ∩ cin 3904   × cxp 5659   ↾ cres 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3910  df-in 3912  df-res 5673

This theorem is referenced by:  relresdm1  6035  imaundir  6148  fresaunres2  6750  fvunsn  7177  fvsnun1  7180  fvsnun2  7181  fsnunfv  7185  fsnunres  7186  frrlem12  8290  domss2  9120  axdc3lem4  10432  fseq1p1m1  13622  hashgval  14365  hashinf  14367  setsres  17233  setscom  17235  setsid  17262  pwssplit1  21180  nosupbnd2lem1  27879  noinfbnd2lem1  27894  noetasuplem2  27898  noetasuplem3  27899  noetasuplem4  27900  noetainflem2  27902  ex-res  30792  padct  33063  eulerpartlemt  34761  poimirlem3  38294  ecunres  39063  mapfzcons1  43468  diophrw  43510  eldioph2lem1  43511  eldioph2lem2  43512  diophin  43523  pwssplit4  43836