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

Theorem resundir 5286
Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
Assertion
Ref Expression
resundir  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  |`  C )  u.  ( B  |`  C ) )

Proof of Theorem resundir
StepHypRef Expression
1 indir 3746 . 2  |-  ( ( A  u.  B )  i^i  ( C  X.  _V ) )  =  ( ( A  i^i  ( C  X.  _V ) )  u.  ( B  i^i  ( C  X.  _V )
) )
2 df-res 5011 . 2  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  u.  B
)  i^i  ( C  X.  _V ) )
3 df-res 5011 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
4 df-res 5011 . . 3  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
53, 4uneq12i 3656 . 2  |-  ( ( A  |`  C )  u.  ( B  |`  C ) )  =  ( ( A  i^i  ( C  X.  _V ) )  u.  ( B  i^i  ( C  X.  _V )
) )
61, 2, 53eqtr4i 2506 1  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  |`  C )  u.  ( B  |`  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   _Vcvv 3113    u. cun 3474    i^i cin 3475    X. cxp 4997    |` cres 5001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-res 5011
This theorem is referenced by:  imaundir  5417  fresaunres2  5755  fvunsn  6091  fvsnun1  6094  fvsnun2  6095  fsnunfv  6099  fsnunres  6100  domss2  7673  axdc3lem4  8829  fseq1p1m1  11748  hashgval  12372  hashinf  12374  setsres  14514  setscom  14516  setsid  14527  pwssplit1  17488  constr3pthlem1  24331  ex-res  24839  eulerpartlemt  27950  wfrlem14  28933  mapfzcons1  30253  diophrw  30296  eldioph2lem1  30297  eldioph2lem2  30298  diophin  30310  pwssplit4  30639
  Copyright terms: Public domain W3C validator