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

Theorem resundir 5569
 Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
Assertion
Ref Expression
resundir ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))

Proof of Theorem resundir
StepHypRef Expression
1 indir 4018 . 2 ((𝐴𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
2 df-res 5278 . 2 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐵) ∩ (𝐶 × V))
3 df-res 5278 . . 3 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
4 df-res 5278 . . 3 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
53, 4uneq12i 3908 . 2 ((𝐴𝐶) ∪ (𝐵𝐶)) = ((𝐴 ∩ (𝐶 × V)) ∪ (𝐵 ∩ (𝐶 × V)))
61, 2, 53eqtr4i 2792 1 ((𝐴𝐵) ↾ 𝐶) = ((𝐴𝐶) ∪ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1632  Vcvv 3340   ∪ cun 3713   ∩ cin 3714   × cxp 5264   ↾ cres 5268 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-in 3722  df-res 5278 This theorem is referenced by:  imaundir  5704  fresaunres2  6237  fvunsn  6610  fvsnun1  6613  fvsnun2  6614  fsnunfv  6618  fsnunres  6619  wfrlem14  7598  domss2  8286  axdc3lem4  9487  fseq1p1m1  12627  hashgval  13334  hashinf  13336  setsres  16123  setscom  16125  setsid  16136  pwssplit1  19281  ex-res  27630  funresdm1  29744  padct  29827  eulerpartlemt  30763  nosupbnd2lem1  32188  noetalem2  32191  noetalem3  32192  poimirlem3  33743  mapfzcons1  37800  diophrw  37842  eldioph2lem1  37843  eldioph2lem2  37844  diophin  37856  pwssplit4  38179
 Copyright terms: Public domain W3C validator