Theorem resundir 5959

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

Syntax hints:   = wceq 1542  Vcvv 3429   ∪ cun 3887   ∩ cin 3888   × cxp 5629   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-in 3896  df-res 5643

This theorem is referenced by:  relresdm1  5998  imaundir  6114  fresaunres2  6712  fvunsn  7134  fvsnun1  7137  fvsnun2  7138  fsnunfv  7142  fsnunres  7143  frrlem12  8247  domss2  9074  axdc3lem4  10375  fseq1p1m1  13552  hashgval  14295  hashinf  14297  setsres  17148  setscom  17150  setsid  17177  pwssplit1  21054  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem2  27698  noetasuplem3  27699  noetasuplem4  27700  noetainflem2  27702  ex-res  30511  padct  32791  eulerpartlemt  34515  poimirlem3  37944  ecunres  38715  mapfzcons1  43149  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  diophin  43204  pwssplit4  43517