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

Theorem resundi 5566
 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 5327 . . . 4 ((𝐵𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
21ineq2i 3952 . . 3 (𝐴 ∩ ((𝐵𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3 indi 4014 . . 3 (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
42, 3eqtri 2780 . 2 (𝐴 ∩ ((𝐵𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5 df-res 5276 . 2 (𝐴 ↾ (𝐵𝐶)) = (𝐴 ∩ ((𝐵𝐶) × V))
6 df-res 5276 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
7 df-res 5276 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
86, 7uneq12i 3906 . 2 ((𝐴𝐵) ∪ (𝐴𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
94, 5, 83eqtr4i 2790 1 (𝐴 ↾ (𝐵𝐶)) = ((𝐴𝐵) ∪ (𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1630  Vcvv 3338   ∪ cun 3711   ∩ cin 3712   × cxp 5262   ↾ cres 5266 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-un 3718  df-in 3720  df-opab 4863  df-xp 5270  df-res 5276 This theorem is referenced by:  imaundi  5701  relresfld  5821  resasplit  6233  fresaunres2  6235  residpr  6570  fnsnsplit  6612  tfrlem16  7656  mapunen  8292  fnfi  8401  fseq1p1m1  12605  resunimafz0  13419  gsum2dlem2  18568  dprd2da  18639  evlseu  19716  ptuncnv  21810  mbfres2  23609  ffsrn  29811  resf1o  29812  cvmliftlem10  31581  eqfunresadj  31964  nosupbnd2lem1  32165  poimirlem9  33729  eldioph4b  37875  pwssplit4  38159  undmrnresiss  38410  relexp0a  38508  rnresun  39859
 Copyright terms: Public domain W3C validator