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

Proof of Theorem resundi
StepHypRef Expression
1 xpundir 4960 . . . 4
21ineq2i 3525 . . 3
3 indi 3572 . . 3
42, 3eqtri 2462 . 2
5 df-res 4919 . 2
6 df-res 4919 . . 3
7 df-res 4919 . . 3
86, 7uneq12i 3485 . 2
94, 5, 83eqtr4i 2472 1
 Colors of variables: wff set class Syntax hints:   wceq 1653  cvv 2962   cun 3304   cin 3305   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