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

Theorem indir 3505
Description: Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
indir  |-  ( ( A  u.  B )  i^i  C )  =  ( ( A  i^i  C )  u.  ( B  i^i  C ) )

Proof of Theorem indir
StepHypRef Expression
1 indi 3503 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3449 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3449 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3449 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3415 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2396 1  |-  ( ( A  u.  B )  i^i  C )  =  ( ( A  i^i  C )  u.  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1647    u. cun 3236    i^i cin 3237
This theorem is referenced by:  difundir  3510  undisj1  3594  disjpr2  3785  resundir  5073  cdaassen  7955  fin23lem26  8098  fpwwe2lem13  8411  fiuncmp  17348  consuba  17363  trfil2  17795  tsmsres  18039  volun  19117  uniioombllem3  19155  itgsplitioo  19407  ppiprm  20612  chtprm  20614  chtdif  20619  ppidif  20624  trust  23853  restmetu  23935  ballotlemfp1  24318  ballotlemgun  24351  predun  25016  fixun  25275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-un 3243  df-in 3245
  Copyright terms: Public domain W3C validator