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

Theorem resundir 5521
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 3983 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5230 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5230 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5230 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 3873 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2756 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1596  Vcvv 3304  cun 3678  cin 3679   × cxp 5216  cres 5220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685  df-in 3687  df-res 5230
This theorem is referenced by:  imaundir  5656  fresaunres2  6189  fvunsn  6561  fvsnun1  6564  fvsnun2  6565  fsnunfv  6569  fsnunres  6570  wfrlem14  7548  domss2  8235  axdc3lem4  9388  fseq1p1m1  12528  hashgval  13235  hashinf  13237  setsres  16024  setscom  16026  setsid  16037  pwssplit1  19182  ex-res  27530  funresdm1  29644  padct  29727  eulerpartlemt  30663  nosupbnd2lem1  32088  noetalem2  32091  noetalem3  32092  poimirlem3  33644  mapfzcons1  37699  diophrw  37741  eldioph2lem1  37742  eldioph2lem2  37743  diophin  37755  pwssplit4  38078
  Copyright terms: Public domain W3C validator