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

Theorem resundi 4922
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 4695 . . . 4  |-  ( ( B  u.  C )  X.  _V )  =  ( ( B  X.  _V )  u.  ( C  X.  _V ) )
21ineq2i 3309 . . 3  |-  ( A  i^i  ( ( B  u.  C )  X. 
_V ) )  =  ( A  i^i  (
( B  X.  _V )  u.  ( C  X.  _V ) ) )
3 indi 3357 . . 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 2276 . 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 4646 . 2  |-  ( A  |`  ( B  u.  C
) )  =  ( A  i^i  ( ( B  u.  C )  X.  _V ) )
6 df-res 4646 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
7 df-res 4646 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
86, 7uneq12i 3269 . 2  |-  ( ( A  |`  B )  u.  ( A  |`  C ) )  =  ( ( A  i^i  ( B  X.  _V ) )  u.  ( A  i^i  ( C  X.  _V )
) )
94, 5, 83eqtr4i 2286 1  |-  ( A  |`  ( B  u.  C
) )  =  ( ( A  |`  B )  u.  ( A  |`  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1619   _Vcvv 2740    u. cun 3092    i^i cin 3093    X. cxp 4624    |` cres 4628
This theorem is referenced by:  imaundi  5046  relresfld  5151  relcoi1  5153  resasplit  5314  fresaunres2  5316  fnsnsplit  5616  tfrlem16  6342  mapunen  6963  fnfi  7067  fseq1p1m1  10788  gsum2d  15150  dprd2da  15204  ptuncnv  17425  mbfres2  18927  evlseu  19327  cvmliftlem10  23162  eupath2lem3  23240  eldioph4b  26226  pwssplit4  26523
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-un 3099  df-in 3101  df-opab 4018  df-xp 4640  df-res 4646
  Copyright terms: Public domain W3C validator