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

Theorem indir 3418
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 3416 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3362 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3362 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3362 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3328 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2314 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 1623    u. cun 3151    i^i cin 3152
This theorem is referenced by:  difundir  3423  undisj1  3507  resundir  4969  cdaassen  7804  fin23lem26  7947  fpwwe2lem13  8260  fiuncmp  17127  consuba  17142  trfil2  17578  tsmsres  17822  volun  18898  uniioombllem3  18936  itgsplitioo  19188  ppiprm  20385  chtprm  20387  chtdif  20392  ppidif  20397  ballotlemfp1  23046  ballotlemgun  23079  predun  23594  fixun  23860  hdrmp  25117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-in 3160
  Copyright terms: Public domain W3C validator