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

Theorem resundi 5865
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 5619 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
21ineq2i 4189 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3 indi 4253 . . 3 (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
42, 3eqtri 2848 . 2 (𝐴 ∩ ((𝐵𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5 df-res 5565 . 2 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
6 df-res 5565 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
7 df-res 5565 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
86, 7uneq12i 4140 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
94, 5, 83eqtr4i 2858 1 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  Vcvv 3499  cun 3937  cin 3938   × cxp 5551  cres 5555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-un 3944  df-in 3946  df-opab 5125  df-xp 5559  df-res 5565
This theorem is referenced by:  imaundi  6005  relresfld  6124  resasplit  6544  fresaunres2  6546  residpr  6900  fnsnsplit  6945  tfrlem16  8023  mapunen  8678  fnfi  8788  fseq1p1m1  12974  resunimafz0  13796  gsum2dlem2  19013  dprd2da  19086  evlseu  20216  ptuncnv  22333  mbfres2  24163  reldisjun  30270  ffsrn  30380  resf1o  30381  symgcom  30643  tocyc01  30676  cvmliftlem10  32427  eqfunresadj  32890  nosupbnd2lem1  33101  poimirlem9  34770  eldioph4b  39275  pwssplit4  39556  undmrnresiss  39831  relexp0a  39928  rnresun  41303
  Copyright terms: Public domain W3C validator