Theorem resundir 5968

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

Syntax hints:   = wceq 1540  Vcvv 3450   ∪ cun 3915   ∩ cin 3916   × cxp 5639   ↾ cres 5643

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3922  df-in 3924  df-res 5653

This theorem is referenced by:  relresdm1  6007  imaundir  6126  fresaunres2  6735  fvunsn  7156  fvsnun1  7159  fvsnun2  7160  fsnunfv  7164  fsnunres  7165  frrlem12  8279  domss2  9106  axdc3lem4  10413  fseq1p1m1  13566  hashgval  14305  hashinf  14307  setsres  17155  setscom  17157  setsid  17184  pwssplit1  20973  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetasuplem2  27653  noetasuplem3  27654  noetasuplem4  27655  noetainflem2  27657  ex-res  30377  padct  32650  eulerpartlemt  34369  poimirlem3  37624  mapfzcons1  42712  diophrw  42754  eldioph2lem1  42755  eldioph2lem2  42756  diophin  42767  pwssplit4  43085