Theorem resundir 5996

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

Syntax hints:   = wceq 1541  Vcvv 3474   ∪ cun 3946   ∩ cin 3947   × cxp 5674   ↾ cres 5678

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-un 3953  df-in 3955  df-res 5688

This theorem is referenced by:  relresdm1  6033  imaundir  6150  fresaunres2  6763  fvunsn  7179  fvsnun1  7182  fvsnun2  7183  fsnunfv  7187  fsnunres  7188  frrlem12  8284  wfrlem14OLD  8324  domss2  9138  axdc3lem4  10450  fseq1p1m1  13577  hashgval  14295  hashinf  14297  setsres  17113  setscom  17115  setsid  17143  pwssplit1  20675  nosupbnd2lem1  27225  noinfbnd2lem1  27240  noetasuplem2  27244  noetasuplem3  27245  noetasuplem4  27246  noetainflem2  27248  ex-res  29732  padct  31982  eulerpartlemt  33439  poimirlem3  36577  mapfzcons1  41537  diophrw  41579  eldioph2lem1  41580  eldioph2lem2  41581  diophin  41592  pwssplit4  41913