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

Theorem resundir 5622
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 4084 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5330 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5330 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5330 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 3971 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2845 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  Vcvv 3398  cun 3774  cin 3775   × cxp 5316  cres 5320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-un 3781  df-in 3783  df-res 5330
This theorem is referenced by:  imaundir  5764  fresaunres2  6294  fvunsn  6673  fvsnun1  6676  fvsnun2  6677  fsnunfv  6681  fsnunres  6682  wfrlem14  7667  domss2  8361  axdc3lem4  9563  fseq1p1m1  12640  hashgval  13343  hashinf  13345  setsres  16115  setscom  16117  setsid  16128  pwssplit1  19269  ex-res  27635  funresdm1  29747  padct  29830  eulerpartlemt  30764  nosupbnd2lem1  32187  noetalem2  32190  noetalem3  32191  poimirlem3  33727  mapfzcons1  37783  diophrw  37825  eldioph2lem1  37826  eldioph2lem2  37827  diophin  37839  pwssplit4  38161
  Copyright terms: Public domain W3C validator