Theorem resundir 6024

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

Syntax hints:   = wceq 1537  Vcvv 3488   ∪ cun 3974   ∩ cin 3975   × cxp 5698   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-in 3983  df-res 5712

This theorem is referenced by:  relresdm1  6062  imaundir  6182  fresaunres2  6793  fvunsn  7213  fvsnun1  7216  fvsnun2  7217  fsnunfv  7221  fsnunres  7222  frrlem12  8338  wfrlem14OLD  8378  domss2  9202  axdc3lem4  10522  fseq1p1m1  13658  hashgval  14382  hashinf  14384  setsres  17225  setscom  17227  setsid  17255  pwssplit1  21081  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem2  27797  noetasuplem3  27798  noetasuplem4  27799  noetainflem2  27801  ex-res  30473  padct  32733  eulerpartlemt  34336  poimirlem3  37583  mapfzcons1  42673  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  diophin  42728  pwssplit4  43046