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

Theorem resundir 5707
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 4134 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5412 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5412 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5412 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 4022 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2806 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1507  Vcvv 3409  cun 3823  cin 3824   × cxp 5398  cres 5402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-un 3830  df-in 3832  df-res 5412
This theorem is referenced by:  imaundir  5843  fresaunres2  6373  fvunsn  6758  fvsnun1  6763  fvsnun2  6764  fvsnun1OLD  6765  fvsnun2OLD  6766  fsnunfv  6770  fsnunres  6771  wfrlem14  7765  domss2  8464  axdc3lem4  9665  fseq1p1m1  12790  hashgval  13501  hashinf  13503  setsres  16371  setscom  16373  setsid  16384  pwssplit1  19543  ex-res  27988  funresdm1  30109  padct  30196  eulerpartlemt  31231  frrlem12  32595  nosupbnd2lem1  32676  noetalem2  32679  noetalem3  32680  poimirlem3  34284  mapfzcons1  38654  diophrw  38696  eldioph2lem1  38697  eldioph2lem2  38698  diophin  38710  pwssplit4  39030
  Copyright terms: Public domain W3C validator