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

Theorem resundi 5996
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 5746 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
21ineq2i 4210 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3 indi 4274 . . 3 (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
42, 3eqtri 2761 . 2 (𝐴 ∩ ((𝐵𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5 df-res 5689 . 2 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
6 df-res 5689 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
7 df-res 5689 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
86, 7uneq12i 4162 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
94, 5, 83eqtr4i 2771 1 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  Vcvv 3475  cun 3947  cin 3948   × cxp 5675  cres 5679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-in 3956  df-opab 5212  df-xp 5683  df-res 5689
This theorem is referenced by:  reldisjun  6033  imaundi  6150  relresfld  6276  resasplit  6762  fresaunres2  6764  residpr  7141  fnsnsplit  7182  eqfunresadj  7357  tfrlem16  8393  mapunen  9146  fnfi  9181  fseq1p1m1  13575  resunimafz0  14404  gsum2dlem2  19839  dprd2da  19912  evlseu  21646  ptuncnv  23311  mbfres2  25162  nosupbnd2lem1  27218  noinfbnd2lem1  27233  ffsrn  31954  resf1o  31955  symgcom  32244  tocyc01  32277  cvmliftlem10  34285  poimirlem9  36497  disjresundif  37109  eldioph4b  41549  pwssplit4  41831  tfsconcatrev  42098  undmrnresiss  42355  relexp0a  42467  rnresun  43876
  Copyright terms: Public domain W3C validator