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

Theorem resundir 5950
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 4233 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5643 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5643 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5643 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 4119 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2775 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  Vcvv 3443  cun 3906  cin 3907   × cxp 5629  cres 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-un 3913  df-in 3915  df-res 5643
This theorem is referenced by:  imaundir  6101  fresaunres2  6711  fvunsn  7121  fvsnun1  7124  fvsnun2  7125  fsnunfv  7129  fsnunres  7130  frrlem12  8220  wfrlem14OLD  8260  domss2  9038  axdc3lem4  10347  fseq1p1m1  13469  hashgval  14187  hashinf  14189  setsres  17010  setscom  17012  setsid  17040  pwssplit1  20473  nosupbnd2lem1  27015  noinfbnd2lem1  27030  noetasuplem2  27034  noetasuplem3  27035  noetasuplem4  27036  noetainflem2  27038  ex-res  29214  funresdm1  31352  padct  31462  eulerpartlemt  32783  poimirlem3  36019  mapfzcons1  40949  diophrw  40991  eldioph2lem1  40992  eldioph2lem2  40993  diophin  41004  pwssplit4  41325
  Copyright terms: Public domain W3C validator