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

Theorem resundi 5949
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 5699 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
21ineq2i 4167 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3 indi 4231 . . 3 (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
42, 3eqtri 2764 . 2 (𝐴 ∩ ((𝐵𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5 df-res 5643 . 2 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
6 df-res 5643 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
7 df-res 5643 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
86, 7uneq12i 4119 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
94, 5, 83eqtr4i 2774 1 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  Vcvv 3443  cun 3906  cin 3907   × cxp 5629  cres 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-un 3913  df-in 3915  df-opab 5166  df-xp 5637  df-res 5643
This theorem is referenced by:  imaundi  6100  relresfld  6226  resasplit  6709  fresaunres2  6711  residpr  7085  fnsnsplit  7126  eqfunresadj  7301  tfrlem16  8335  mapunen  9086  fnfi  9121  fseq1p1m1  13507  resunimafz0  14334  gsum2dlem2  19739  dprd2da  19812  evlseu  21477  ptuncnv  23142  mbfres2  24993  nosupbnd2lem1  27047  noinfbnd2lem1  27062  reldisjun  31407  ffsrn  31529  resf1o  31530  symgcom  31817  tocyc01  31850  cvmliftlem10  33757  poimirlem9  36054  disjresundif  36667  eldioph4b  41072  pwssplit4  41354  undmrnresiss  41818  relexp0a  41930  rnresun  43333
  Copyright terms: Public domain W3C validator