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

Theorem resundi 5208
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 4976 . . . 4  |-  ( ( B  u.  C )  X.  _V )  =  ( ( B  X.  _V )  u.  ( C  X.  _V ) )
21ineq2i 3633 . . 3  |-  ( A  i^i  ( ( B  u.  C )  X. 
_V ) )  =  ( A  i^i  (
( B  X.  _V )  u.  ( C  X.  _V ) ) )
3 indi 3680 . . 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 2478 . 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 4936 . 2  |-  ( A  |`  ( B  u.  C
) )  =  ( A  i^i  ( ( B  u.  C )  X.  _V ) )
6 df-res 4936 . . 3  |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V ) )
7 df-res 4936 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
86, 7uneq12i 3592 . 2  |-  ( ( A  |`  B )  u.  ( A  |`  C ) )  =  ( ( A  i^i  ( B  X.  _V ) )  u.  ( A  i^i  ( C  X.  _V )
) )
94, 5, 83eqtr4i 2488 1  |-  ( A  |`  ( B  u.  C
) )  =  ( ( A  |`  B )  u.  ( A  |`  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   _Vcvv 3054    u. cun 3410    i^i cin 3411    X. cxp 4922    |` cres 4926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-v 3056  df-un 3417  df-in 3419  df-opab 4435  df-xp 4930  df-res 4936
This theorem is referenced by:  imaundi  5333  relresfld  5448  relcoi1  5450  resasplit  5665  fresaunres2  5667  residpr  5971  fnsnsplit  6000  tfrlem16  6938  mapunen  7566  fnfi  7676  fseq1p1m1  11621  gsum2dlem2  16553  gsum2dOLD  16555  dprd2da  16632  evlseu  17695  ptuncnv  19482  mbfres2  21225  eupath2lem3  23721  ffsrn  26149  resf1o  26150  cvmliftlem10  27303  eldioph4b  29274  pwssplit4  29566
  Copyright terms: Public domain W3C validator