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

Theorem resundi 5292
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 5058 . . . 4
21ineq2i 3696 . . 3
3 indi 3743 . . 3
42, 3eqtri 2486 . 2
5 df-res 5016 . 2
6 df-res 5016 . . 3
7 df-res 5016 . . 3
86, 7uneq12i 3655 . 2
94, 5, 83eqtr4i 2496 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395   cvv 3109  u.cun 3473  i^icin 3474  X.cxp 5002  |`cres 5006
This theorem is referenced by:  imaundi  5423  relresfld  5539  relcoi1  5541  resasplit  5760  fresaunres2  5762  residpr  6075  fnsnsplit  6108  tfrlem16  7081  mapunen  7706  fnfi  7818  fseq1p1m1  11781  gsum2dlem2  16998  gsum2dOLD  17000  dprd2da  17091  evlseu  18185  ptuncnv  20308  mbfres2  22052  eupath2lem3  24979  ffsrn  27552  resf1o  27553  cvmliftlem10  28739  eldioph4b  30745  pwssplit4  31035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-opab 4511  df-xp 5010  df-res 5016
  Copyright terms: Public domain W3C validator