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

Theorem indir 3593
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 3591 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3538 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3538 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3538 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3503 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2468 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 1369    u. cun 3321    i^i cin 3322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-in 3330
This theorem is referenced by:  difundir  3598  undisj1  3725  disjpr2  3933  resundir  5120  cdaassen  8343  fin23lem26  8486  fpwwe2lem13  8801  neitr  18759  fiuncmp  18982  consuba  18999  trfil2  19435  tsmsresOLD  19692  tsmsres  19693  trust  19779  restmetu  20137  volun  21001  uniioombllem3  21040  itgsplitioo  21290  ppiprm  22464  chtprm  22466  chtdif  22471  ppidif  22476  ballotlemfp1  26826  ballotlemgun  26859  predun  27602  fixun  27891  mbfposadd  28392
  Copyright terms: Public domain W3C validator