MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resundir Structured version   Visualization version   GIF version

Theorem resundir 5318
Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
Assertion
Ref Expression
resundir ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))

Proof of Theorem resundir
StepHypRef Expression
1 indir 3833 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5040 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5040 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5040 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 3726 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2641 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  Vcvv 3172  cun 3537  cin 3538   × cxp 5026  cres 5030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-res 5040
This theorem is referenced by:  imaundir  5451  fresaunres2  5974  fvunsn  6328  fvsnun1  6331  fvsnun2  6332  fsnunfv  6336  fsnunres  6337  wfrlem14  7292  domss2  7981  axdc3lem4  9135  fseq1p1m1  12238  hashgval  12937  hashinf  12939  setsres  15675  setscom  15677  setsid  15688  pwssplit1  18826  constr3pthlem1  25949  ex-res  26456  padct  28691  eulerpartlemt  29566  poimirlem3  32378  mapfzcons1  36094  diophrw  36136  eldioph2lem1  36137  eldioph2lem2  36138  diophin  36150  pwssplit4  36473
  Copyright terms: Public domain W3C validator