Theorem resundir 5957

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

Syntax hints:   = wceq 1541  Vcvv 3446   ∪ cun 3911   ∩ cin 3912   × cxp 5636   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-un 3918  df-in 3920  df-res 5650

This theorem is referenced by:  imaundir  6108  fresaunres2  6719  fvunsn  7130  fvsnun1  7133  fvsnun2  7134  fsnunfv  7138  fsnunres  7139  frrlem12  8233  wfrlem14OLD  8273  domss2  9087  axdc3lem4  10398  fseq1p1m1  13525  hashgval  14243  hashinf  14245  setsres  17061  setscom  17063  setsid  17091  pwssplit1  20577  nosupbnd2lem1  27100  noinfbnd2lem1  27115  noetasuplem2  27119  noetasuplem3  27120  noetasuplem4  27121  noetainflem2  27123  ex-res  29448  funresdm1  31590  padct  31704  eulerpartlemt  33060  poimirlem3  36154  mapfzcons1  41098  diophrw  41140  eldioph2lem1  41141  eldioph2lem2  41142  diophin  41153  pwssplit4  41474