Theorem resundir 5951

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

Syntax hints:   = wceq 1541  Vcvv 3438   ∪ cun 3897   ∩ cin 3898   × cxp 5620   ↾ cres 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-un 3904  df-in 3906  df-res 5634

This theorem is referenced by:  relresdm1  5990  imaundir  6106  fresaunres2  6704  fvunsn  7123  fvsnun1  7126  fvsnun2  7127  fsnunfv  7131  fsnunres  7132  frrlem12  8237  domss2  9062  axdc3lem4  10361  fseq1p1m1  13512  hashgval  14254  hashinf  14256  setsres  17103  setscom  17105  setsid  17132  pwssplit1  21009  nosupbnd2lem1  27681  noinfbnd2lem1  27696  noetasuplem2  27700  noetasuplem3  27701  noetasuplem4  27702  noetainflem2  27704  ex-res  30465  padct  32746  eulerpartlemt  34477  poimirlem3  37763  ecunres  38518  mapfzcons1  42901  diophrw  42943  eldioph2lem1  42944  eldioph2lem2  42945  diophin  42956  pwssplit4  43273