Theorem resundir 5895

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

Syntax hints:   = wceq 1539  Vcvv 3422   ∪ cun 3881   ∩ cin 3882   × cxp 5578   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-in 3890  df-res 5592

This theorem is referenced by:  imaundir  6043  fresaunres2  6630  fvunsn  7033  fvsnun1  7036  fvsnun2  7037  fsnunfv  7041  fsnunres  7042  frrlem12  8084  wfrlem14OLD  8124  domss2  8872  axdc3lem4  10140  fseq1p1m1  13259  hashgval  13975  hashinf  13977  setsres  16807  setscom  16809  setsid  16837  pwssplit1  20236  ex-res  28706  funresdm1  30845  padct  30956  eulerpartlemt  32238  nosupbnd2lem1  33845  noinfbnd2lem1  33860  noetasuplem2  33864  noetasuplem3  33865  noetasuplem4  33866  noetainflem2  33868  poimirlem3  35707  mapfzcons1  40455  diophrw  40497  eldioph2lem1  40498  eldioph2lem2  40499  diophin  40510  pwssplit4  40830