Theorem resundir 6001

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

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3454   ∩ cin 4092   ∪ cun 4152   × cxp 5656   ↾ cres 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-in 4094  df-un 4154  df-res 5670

This theorem is used by:  relresdm1  6043  imaundir  6160  fresaunres2  6784  fvunsn  7215  fvsnun1  7218  fvsnun2  7219  fsnunfv  7223  fsnunres  7224  frrlem12  8353  domss2  9193  axdc3lem4  10570  fseq1p1m1  13772  hashgval  14518  hashinf  14520  setsres  17400  setscom  17402  setsid  17429  pwssplit1  21385  nosupbnd2lem1  28129  noinfbnd2lem1  28144  noetasuplem2  28148  noetasuplem3  28149  noetasuplem4  28150  noetainflem2  28152  ex-res  31099  padct  33407  eulerpartlemt  35114  poimirlem3  38809  ecunres  39592  mapfzcons1  43994  diophrw  44036  eldioph2lem1  44037  eldioph2lem2  44038  diophin  44049  pwssplit4  44357