Theorem resundir 5954

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

Syntax hints:   = wceq 1540  Vcvv 3444   ∪ cun 3909   ∩ cin 3910   × cxp 5629   ↾ cres 5633

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-un 3916  df-in 3918  df-res 5643

This theorem is referenced by:  relresdm1  5993  imaundir  6111  fresaunres2  6714  fvunsn  7135  fvsnun1  7138  fvsnun2  7139  fsnunfv  7143  fsnunres  7144  frrlem12  8253  domss2  9077  axdc3lem4  10382  fseq1p1m1  13535  hashgval  14274  hashinf  14276  setsres  17124  setscom  17126  setsid  17153  pwssplit1  20998  nosupbnd2lem1  27660  noinfbnd2lem1  27675  noetasuplem2  27679  noetasuplem3  27680  noetasuplem4  27681  noetainflem2  27683  ex-res  30420  padct  32693  eulerpartlemt  34355  poimirlem3  37610  mapfzcons1  42698  diophrw  42740  eldioph2lem1  42741  eldioph2lem2  42742  diophin  42753  pwssplit4  43071