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

Theorem resundi 5100
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 4871 . . . 4  |-  ( ( B  u.  C )  X.  _V )  =  ( ( B  X.  _V )  u.  ( C  X.  _V ) )
21ineq2i 3482 . . 3  |-  ( A  i^i  ( ( B  u.  C )  X. 
_V ) )  =  ( A  i^i  (
( B  X.  _V )  u.  ( C  X.  _V ) ) )
3 indi 3530 . . 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 2407 . 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 4830 . 2  |-  ( A  |`  ( B  u.  C
) )  =  ( A  i^i  ( ( B  u.  C )  X.  _V ) )
6 df-res 4830 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
7 df-res 4830 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
86, 7uneq12i 3442 . 2  |-  ( ( A  |`  B )  u.  ( A  |`  C ) )  =  ( ( A  i^i  ( B  X.  _V ) )  u.  ( A  i^i  ( C  X.  _V )
) )
94, 5, 83eqtr4i 2417 1  |-  ( A  |`  ( B  u.  C
) )  =  ( ( A  |`  B )  u.  ( A  |`  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1649   _Vcvv 2899    u. cun 3261    i^i cin 3262    X. cxp 4816    |` cres 4820
This theorem is referenced by:  imaundi  5224  relresfld  5336  relcoi1  5338  resasplit  5553  fresaunres2  5555  fnsnsplit  5869  tfrlem16  6590  mapunen  7212  fnfi  7320  fseq1p1m1  11052  gsum2d  15473  dprd2da  15527  ptuncnv  17760  mbfres2  19404  evlseu  19804  eupath2lem3  21549  cvmliftlem10  24760  eldioph4b  26563  pwssplit4  26860
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-un 3268  df-in 3270  df-opab 4208  df-xp 4824  df-res 4830
  Copyright terms: Public domain W3C validator