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

Theorem indir 3739
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 3737 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3684 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3684 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3684 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3649 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2499 1  |-  ( ( A  u.  B )  i^i  C )  =  ( ( A  i^i  C )  u.  ( B  i^i  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374    u. cun 3467    i^i cin 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-in 3476
This theorem is referenced by:  difundir  3744  undisj1  3871  disjpr2  4083  resundir  5279  cdaassen  8551  fin23lem26  8694  fpwwe2lem13  9009  neitr  19440  fiuncmp  19663  consuba  19680  trfil2  20116  tsmsresOLD  20373  tsmsres  20374  trust  20460  restmetu  20818  volun  21683  uniioombllem3  21722  itgsplitioo  21972  ppiprm  23146  chtprm  23148  chtdif  23153  ppidif  23158  ballotlemfp1  27920  ballotlemgun  27953  predun  28697  fixun  28986  mbfposadd  29490
  Copyright terms: Public domain W3C validator