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

Theorem resundir 4970
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 3417 . 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 4701 . 2  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  u.  B
)  i^i  ( C  X.  _V ) )
3 df-res 4701 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
4 df-res 4701 . . 3  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
53, 4uneq12i 3327 . 2  |-  ( ( A  |`  C )  u.  ( B  |`  C ) )  =  ( ( A  i^i  ( C  X.  _V ) )  u.  ( B  i^i  ( C  X.  _V )
) )
61, 2, 53eqtr4i 2313 1  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  |`  C )  u.  ( B  |`  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1623   _Vcvv 2788    u. cun 3150    i^i cin 3151    X. cxp 4687    |` cres 4691
This theorem is referenced by:  imaundir  5094  fresaunres2  5413  fvunsn  5712  fvsnun1  5715  fvsnun2  5716  fsnunfv  5720  fsnunres  5721  domss2  7020  axdc3lem4  8079  fseq1p1m1  10857  hashgval  11340  hashinf  11342  setsres  13174  setscom  13176  setsid  13187  ex-res  20828  wfrlem14  24269  mapfzcons1  26794  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  diophin  26852  pwssplit1  27188  pwssplit4  27191
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-res 4701
  Copyright terms: Public domain W3C validator