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

Theorem resundir 5276
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 3743 . 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 5000 . 2  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  u.  B
)  i^i  ( C  X.  _V ) )
3 df-res 5000 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
4 df-res 5000 . . 3  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
53, 4uneq12i 3642 . 2  |-  ( ( A  |`  C )  u.  ( B  |`  C ) )  =  ( ( A  i^i  ( C  X.  _V ) )  u.  ( B  i^i  ( C  X.  _V )
) )
61, 2, 53eqtr4i 2493 1  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  |`  C )  u.  ( B  |`  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   _Vcvv 3106    u. cun 3459    i^i cin 3460    X. cxp 4986    |` cres 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-res 5000
This theorem is referenced by:  imaundir  5404  fresaunres2  5739  fvunsn  6079  fvsnun1  6082  fvsnun2  6083  fsnunfv  6087  fsnunres  6088  domss2  7669  axdc3lem4  8824  fseq1p1m1  11756  hashgval  12393  hashinf  12395  setsres  14749  setscom  14751  setsid  14762  pwssplit1  17903  constr3pthlem1  24860  ex-res  25367  padct  27779  eulerpartlemt  28577  wfrlem14  29599  mapfzcons1  30892  diophrw  30934  eldioph2lem1  30935  eldioph2lem2  30936  diophin  30948  pwssplit4  31277
  Copyright terms: Public domain W3C validator