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

Theorem resundir 6012
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 4286 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5697 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5697 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5697 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 4166 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2775 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  Vcvv 3480  cun 3949  cin 3950   × cxp 5683  cres 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-in 3958  df-res 5697
This theorem is referenced by:  relresdm1  6051  imaundir  6170  fresaunres2  6780  fvunsn  7199  fvsnun1  7202  fvsnun2  7203  fsnunfv  7207  fsnunres  7208  frrlem12  8322  wfrlem14OLD  8362  domss2  9176  axdc3lem4  10493  fseq1p1m1  13638  hashgval  14372  hashinf  14374  setsres  17215  setscom  17217  setsid  17244  pwssplit1  21058  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem2  27779  noetasuplem3  27780  noetasuplem4  27781  noetainflem2  27783  ex-res  30460  padct  32731  eulerpartlemt  34373  poimirlem3  37630  mapfzcons1  42728  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  diophin  42783  pwssplit4  43101
  Copyright terms: Public domain W3C validator