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

Theorem resundi 5189
Description: Distributive law for restriction over union. Theorem 31 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
resundi  |-  ( A  |`  ( B  u.  C
) )  =  ( ( A  |`  B )  u.  ( A  |`  C ) )

Proof of Theorem resundi
StepHypRef Expression
1 xpundir 4960 . . . 4  |-  ( ( B  u.  C )  X.  _V )  =  ( ( B  X.  _V )  u.  ( C  X.  _V ) )
21ineq2i 3525 . . 3  |-  ( A  i^i  ( ( B  u.  C )  X. 
_V ) )  =  ( A  i^i  (
( B  X.  _V )  u.  ( C  X.  _V ) ) )
3 indi 3572 . . 3  |-  ( A  i^i  ( ( B  X.  _V )  u.  ( C  X.  _V ) ) )  =  ( ( A  i^i  ( B  X.  _V )
)  u.  ( A  i^i  ( C  X.  _V ) ) )
42, 3eqtri 2462 . 2  |-  ( A  i^i  ( ( B  u.  C )  X. 
_V ) )  =  ( ( A  i^i  ( B  X.  _V )
)  u.  ( A  i^i  ( C  X.  _V ) ) )
5 df-res 4919 . 2  |-  ( A  |`  ( B  u.  C
) )  =  ( A  i^i  ( ( B  u.  C )  X.  _V ) )
6 df-res 4919 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
7 df-res 4919 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
86, 7uneq12i 3485 . 2  |-  ( ( A  |`  B )  u.  ( A  |`  C ) )  =  ( ( A  i^i  ( B  X.  _V ) )  u.  ( A  i^i  ( C  X.  _V )
) )
94, 5, 83eqtr4i 2472 1  |-  ( A  |`  ( B  u.  C
) )  =  ( ( A  |`  B )  u.  ( A  |`  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1653   _Vcvv 2962    u. cun 3304    i^i cin 3305    X. cxp 4905    |` cres 4909
This theorem is referenced by:  imaundi  5313  relresfld  5425  relcoi1  5427  resasplit  5642  fresaunres2  5644  fnsnsplit  5959  tfrlem16  6683  mapunen  7305  fnfi  7413  fseq1p1m1  11153  gsum2d  15577  dprd2da  15631  ptuncnv  17870  mbfres2  19566  evlseu  19968  eupath2lem3  21732  cvmliftlem10  25012  eldioph4b  26910  pwssplit4  27206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311  df-in 3313  df-opab 4292  df-xp 4913  df-res 4919
  Copyright terms: Public domain W3C validator