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

Theorem resundir 5102
Description: Distributive law for restriction over union. (Contributed by NM, 23-Sep-2004.)
Assertion
Ref Expression
resundir  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  |`  C )  u.  ( B  |`  C ) )

Proof of Theorem resundir
StepHypRef Expression
1 indir 3533 . 2  |-  ( ( A  u.  B )  i^i  ( C  X.  _V ) )  =  ( ( A  i^i  ( C  X.  _V ) )  u.  ( B  i^i  ( C  X.  _V )
) )
2 df-res 4831 . 2  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  u.  B
)  i^i  ( C  X.  _V ) )
3 df-res 4831 . . 3  |-  ( A  |`  C )  =  ( A  i^i  ( C  X.  _V ) )
4 df-res 4831 . . 3  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
53, 4uneq12i 3443 . 2  |-  ( ( A  |`  C )  u.  ( B  |`  C ) )  =  ( ( A  i^i  ( C  X.  _V ) )  u.  ( B  i^i  ( C  X.  _V )
) )
61, 2, 53eqtr4i 2418 1  |-  ( ( A  u.  B )  |`  C )  =  ( ( A  |`  C )  u.  ( B  |`  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1649   _Vcvv 2900    u. cun 3262    i^i cin 3263    X. cxp 4817    |` cres 4821
This theorem is referenced by:  imaundir  5226  fresaunres2  5556  fvunsn  5865  fvsnun1  5868  fvsnun2  5869  fsnunfv  5873  fsnunres  5874  domss2  7203  axdc3lem4  8267  fseq1p1m1  11053  hashgval  11549  hashinf  11551  setsres  13423  setscom  13425  setsid  13436  constr3pthlem1  21491  ex-res  21598  wfrlem14  25294  mapfzcons1  26465  diophrw  26509  eldioph2lem1  26510  eldioph2lem2  26511  diophin  26523  pwssplit1  26858  pwssplit4  26861
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-un 3269  df-in 3271  df-res 4831
  Copyright terms: Public domain W3C validator