Theorem resundir 5981

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

Syntax hints:   = wceq 1540  Vcvv 3459   ∪ cun 3924   ∩ cin 3925   × cxp 5652   ↾ cres 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-in 3933  df-res 5666

This theorem is referenced by:  relresdm1  6020  imaundir  6139  fresaunres2  6749  fvunsn  7170  fvsnun1  7173  fvsnun2  7174  fsnunfv  7178  fsnunres  7179  frrlem12  8294  wfrlem14OLD  8334  domss2  9148  axdc3lem4  10465  fseq1p1m1  13613  hashgval  14349  hashinf  14351  setsres  17195  setscom  17197  setsid  17224  pwssplit1  21015  nosupbnd2lem1  27677  noinfbnd2lem1  27692  noetasuplem2  27696  noetasuplem3  27697  noetasuplem4  27698  noetainflem2  27700  ex-res  30368  padct  32643  eulerpartlemt  34349  poimirlem3  37593  mapfzcons1  42687  diophrw  42729  eldioph2lem1  42730  eldioph2lem2  42731  diophin  42742  pwssplit4  43060