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

Theorem indir 3430
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 3428 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3374 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3374 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3374 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3340 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2326 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 1632    u. cun 3163    i^i cin 3164
This theorem is referenced by:  difundir  3435  undisj1  3519  resundir  4986  cdaassen  7824  fin23lem26  7967  fpwwe2lem13  8280  fiuncmp  17147  consuba  17162  trfil2  17598  tsmsres  17842  volun  18918  uniioombllem3  18956  itgsplitioo  19208  ppiprm  20405  chtprm  20407  chtdif  20412  ppidif  20417  ballotlemfp1  23066  ballotlemgun  23099  predun  24261  fixun  24520  hdrmp  25809  disjpr2  28185
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172
  Copyright terms: Public domain W3C validator