Theorem resundir 5707

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

Syntax hints:   = wceq 1507  Vcvv 3409   ∪ cun 3823   ∩ cin 3824   × cxp 5398   ↾ cres 5402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-un 3830  df-in 3832  df-res 5412

This theorem is referenced by:  imaundir  5843  fresaunres2  6373  fvunsn  6758  fvsnun1  6763  fvsnun2  6764  fvsnun1OLD  6765  fvsnun2OLD  6766  fsnunfv  6770  fsnunres  6771  wfrlem14  7765  domss2  8464  axdc3lem4  9665  fseq1p1m1  12790  hashgval  13501  hashinf  13503  setsres  16371  setscom  16373  setsid  16384  pwssplit1  19543  ex-res  27988  funresdm1  30109  padct  30196  eulerpartlemt  31231  frrlem12  32595  nosupbnd2lem1  32676  noetalem2  32679  noetalem3  32680  poimirlem3  34284  mapfzcons1  38654  diophrw  38696  eldioph2lem1  38697  eldioph2lem2  38698  diophin  38710  pwssplit4  39030