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

Theorem indir 3324
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 3322 . 2  |-  ( C  i^i  ( A  u.  B ) )  =  ( ( C  i^i  A )  u.  ( C  i^i  B ) )
2 incom 3269 . 2  |-  ( ( A  u.  B )  i^i  C )  =  ( C  i^i  ( A  u.  B )
)
3 incom 3269 . . 3  |-  ( A  i^i  C )  =  ( C  i^i  A
)
4 incom 3269 . . 3  |-  ( B  i^i  C )  =  ( C  i^i  B
)
53, 4uneq12i 3237 . 2  |-  ( ( A  i^i  C )  u.  ( B  i^i  C ) )  =  ( ( C  i^i  A
)  u.  ( C  i^i  B ) )
61, 2, 53eqtr4i 2283 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 1619    u. cun 3076    i^i cin 3077
This theorem is referenced by:  difundir  3329  undisj1  3413  resundir  4877  cdaassen  7692  fin23lem26  7835  fpwwe2lem13  8144  fiuncmp  16963  consuba  16978  trfil2  17414  tsmsres  17658  volun  18734  uniioombllem3  18772  itgsplitioo  19024  ppiprm  20221  chtprm  20223  chtdif  20228  ppidif  20233  predun  23358  fixun  23624  hdrmp  24872
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-in 3085
  Copyright terms: Public domain W3C validator