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

Theorem indir 3728
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 3726 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3673 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3673 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3673 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3638 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2480 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 1381    u. cun 3456    i^i cin 3457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463  df-in 3465
This theorem is referenced by:  difundir  3733  undisj1  3860  disjpr2  4073  resundir  5274  cdaassen  8560  fin23lem26  8703  fpwwe2lem13  9018  neitr  19547  fiuncmp  19770  consuba  19787  trfil2  20254  tsmsresOLD  20511  tsmsres  20512  trust  20598  restmetu  20956  volun  21821  uniioombllem3  21860  itgsplitioo  22110  ppiprm  23290  chtprm  23292  chtdif  23297  ppidif  23302  ballotlemfp1  28296  ballotlemgun  28329  mrsubvrs  28748  mthmpps  28808  predun  29238  fixun  29527  mbfposadd  30030
  Copyright terms: Public domain W3C validator