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

Theorem resundi 4876
 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 4649 . . . 4
21ineq2i 3275 . . 3
3 indi 3322 . . 3
42, 3eqtri 2273 . 2
5 df-res 4600 . 2
6 df-res 4600 . . 3
7 df-res 4600 . . 3
86, 7uneq12i 3237 . 2
94, 5, 83eqtr4i 2283 1
 Colors of variables: wff set class Syntax hints:   wceq 1619  cvv 2727   cun 3076   cin 3077   cxp 4578   cres 4582 This theorem is referenced by:  imaundi  5000  relresfld  5105  relcoi1  5107  resasplit  5268  fresaunres2  5270  fnsnsplit  5569  tfrlem16  6295  mapunen  6915  fnfi  7019  fseq1p1m1  10735  gsum2d  15058  dprd2da  15112  ptuncnv  17330  mbfres2  18832  evlseu  19232  cvmliftlem10  22996  eupath2lem3  23074  eldioph4b  26060  pwssplit4  26357 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 1926  ax-ext 2234 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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-in 3085  df-opab 3975  df-xp 4594  df-res 4600
 Copyright terms: Public domain W3C validator