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

Theorem indir 3699
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 3697 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3644 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3644 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3644 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3609 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2490 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 1370    u. cun 3427    i^i cin 3428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-un 3434  df-in 3436
This theorem is referenced by:  difundir  3704  undisj1  3831  disjpr2  4039  resundir  5226  cdaassen  8455  fin23lem26  8598  fpwwe2lem13  8913  neitr  18909  fiuncmp  19132  consuba  19149  trfil2  19585  tsmsresOLD  19842  tsmsres  19843  trust  19929  restmetu  20287  volun  21152  uniioombllem3  21191  itgsplitioo  21441  ppiprm  22615  chtprm  22617  chtdif  22622  ppidif  22627  ballotlemfp1  27011  ballotlemgun  27044  predun  27788  fixun  28077  mbfposadd  28580
  Copyright terms: Public domain W3C validator