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

Theorem resundi 4969
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 4742 . . . 4  |-  ( ( B  u.  C )  X.  _V )  =  ( ( B  X.  _V )  u.  ( C  X.  _V ) )
21ineq2i 3367 . . 3  |-  ( A  i^i  ( ( B  u.  C )  X. 
_V ) )  =  ( A  i^i  (
( B  X.  _V )  u.  ( C  X.  _V ) ) )
3 indi 3415 . . 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 2303 . 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 4701 . 2  |-  ( A  |`  ( B  u.  C
) )  =  ( A  i^i  ( ( B  u.  C )  X.  _V ) )
6 df-res 4701 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
7 df-res 4701 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
86, 7uneq12i 3327 . 2  |-  ( ( A  |`  B )  u.  ( A  |`  C ) )  =  ( ( A  i^i  ( B  X.  _V ) )  u.  ( A  i^i  ( C  X.  _V )
) )
94, 5, 83eqtr4i 2313 1  |-  ( A  |`  ( B  u.  C
) )  =  ( ( A  |`  B )  u.  ( A  |`  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1623   _Vcvv 2788    u. cun 3150    i^i cin 3151    X. cxp 4687    |` cres 4691
This theorem is referenced by:  imaundi  5093  relresfld  5199  relcoi1  5201  resasplit  5411  fresaunres2  5413  fnsnsplit  5717  tfrlem16  6409  mapunen  7030  fnfi  7134  fseq1p1m1  10857  gsum2d  15223  dprd2da  15277  ptuncnv  17498  mbfres2  19000  evlseu  19400  cvmliftlem10  23236  eupath2lem3  23314  eldioph4b  26306  pwssplit4  26603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-opab 4078  df-xp 4695  df-res 4701
  Copyright terms: Public domain W3C validator