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

Theorem resundir 5997
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 4276 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5689 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5689 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5689 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 4162 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2771 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  Vcvv 3475  cun 3947  cin 3948   × cxp 5675  cres 5679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-in 3956  df-res 5689
This theorem is referenced by:  relresdm1  6034  imaundir  6151  fresaunres2  6764  fvunsn  7177  fvsnun1  7180  fvsnun2  7181  fsnunfv  7185  fsnunres  7186  frrlem12  8282  wfrlem14OLD  8322  domss2  9136  axdc3lem4  10448  fseq1p1m1  13575  hashgval  14293  hashinf  14295  setsres  17111  setscom  17113  setsid  17141  pwssplit1  20670  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetasuplem2  27237  noetasuplem3  27238  noetasuplem4  27239  noetainflem2  27241  ex-res  29694  padct  31944  eulerpartlemt  33370  poimirlem3  36491  mapfzcons1  41455  diophrw  41497  eldioph2lem1  41498  eldioph2lem2  41499  diophin  41510  pwssplit4  41831
  Copyright terms: Public domain W3C validator