Theorem resundir 5987

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-in 3906  df-res 5667

This theorem is used by:  relresdm1  6029  imaundir  6142  fresaunres2  6748  fvunsn  7178  fvsnun1  7181  fvsnun2  7182  fsnunfv  7186  fsnunres  7187  frrlem12  8297  domss2  9137  axdc3lem4  10458  fseq1p1m1  13656  hashgval  14400  hashinf  14402  setsres  17273  setscom  17275  setsid  17302  pwssplit1  21246  nosupbnd2lem1  27954  noinfbnd2lem1  27969  noetasuplem2  27973  noetasuplem3  27974  noetasuplem4  27975  noetainflem2  27977  ex-res  30924  padct  33192  eulerpartlemt  34885  poimirlem3  38375  ecunres  39145  mapfzcons1  43565  diophrw  43607  eldioph2lem1  43608  eldioph2lem2  43609  diophin  43620  pwssplit4  43933