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

Theorem resundir 5209
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 3682 . 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 4936 . 2  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  u.  B
)  i^i  ( C  X.  _V ) )
3 df-res 4936 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
4 df-res 4936 . . 3  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
53, 4uneq12i 3592 . 2  |-  ( ( A  |`  C )  u.  ( B  |`  C ) )  =  ( ( A  i^i  ( C  X.  _V ) )  u.  ( B  i^i  ( C  X.  _V )
) )
61, 2, 53eqtr4i 2488 1  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  |`  C )  u.  ( B  |`  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   _Vcvv 3054    u. cun 3410    i^i cin 3411    X. cxp 4922    |` cres 4926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-v 3056  df-un 3417  df-in 3419  df-res 4936
This theorem is referenced by:  imaundir  5334  fresaunres2  5667  fvunsn  5995  fvsnun1  5998  fvsnun2  5999  fsnunfv  6003  fsnunres  6004  domss2  7556  axdc3lem4  8709  fseq1p1m1  11621  hashgval  12193  hashinf  12195  setsres  14290  setscom  14292  setsid  14303  pwssplit1  17232  constr3pthlem1  23662  ex-res  23769  eulerpartlemt  26874  wfrlem14  27857  mapfzcons1  29177  diophrw  29221  eldioph2lem1  29222  eldioph2lem2  29223  diophin  29235  pwssplit4  29566
  Copyright terms: Public domain W3C validator