Theorem resundir 5622

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

Syntax hints:   = wceq 1637  Vcvv 3398   ∪ cun 3774   ∩ cin 3775   × cxp 5316   ↾ cres 5320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-un 3781  df-in 3783  df-res 5330

This theorem is referenced by:  imaundir  5764  fresaunres2  6294  fvunsn  6673  fvsnun1  6676  fvsnun2  6677  fsnunfv  6681  fsnunres  6682  wfrlem14  7667  domss2  8361  axdc3lem4  9563  fseq1p1m1  12640  hashgval  13343  hashinf  13345  setsres  16115  setscom  16117  setsid  16128  pwssplit1  19269  ex-res  27635  funresdm1  29747  padct  29830  eulerpartlemt  30764  nosupbnd2lem1  32187  noetalem2  32190  noetalem3  32191  poimirlem3  33727  mapfzcons1  37783  diophrw  37825  eldioph2lem1  37826  eldioph2lem2  37827  diophin  37839  pwssplit4  38161