Theorem resundir 5985

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

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3451   ∪ cun 3897   ∩ cin 3898   × cxp 5649   ↾ cres 5653

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-in 3906  df-res 5663

This theorem is used by:  relresdm1  6025  imaundir  6142  fresaunres2  6754  fvunsn  7184  fvsnun1  7187  fvsnun2  7188  fsnunfv  7192  fsnunres  7193  frrlem12  8315  domss2  9155  axdc3lem4  10531  fseq1p1m1  13732  hashgval  14477  hashinf  14479  setsres  17356  setscom  17358  setsid  17385  pwssplit1  21334  nosupbnd2lem1  28072  noinfbnd2lem1  28087  noetasuplem2  28091  noetasuplem3  28092  noetasuplem4  28093  noetainflem2  28095  ex-res  31042  padct  33310  eulerpartlemt  35003  poimirlem3  38541  ecunres  39326  mapfzcons1  43727  diophrw  43769  eldioph2lem1  43770  eldioph2lem2  43771  diophin  43782  pwssplit4  44090