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

Theorem indi 3428
Description: Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
indi  |-  ( A  i^i  ( B  u.  C ) )  =  ( ( A  i^i  B )  u.  ( A  i^i  C ) )

Proof of Theorem indi
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 andi 837 . . . 4  |-  ( ( x  e.  A  /\  ( x  e.  B  \/  x  e.  C
) )  <->  ( (
x  e.  A  /\  x  e.  B )  \/  ( x  e.  A  /\  x  e.  C
) ) )
2 elin 3371 . . . . 5  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3371 . . . . 5  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
42, 3orbi12i 507 . . . 4  |-  ( ( x  e.  ( A  i^i  B )  \/  x  e.  ( A  i^i  C ) )  <-> 
( ( x  e.  A  /\  x  e.  B )  \/  (
x  e.  A  /\  x  e.  C )
) )
51, 4bitr4i 243 . . 3  |-  ( ( x  e.  A  /\  ( x  e.  B  \/  x  e.  C
) )  <->  ( x  e.  ( A  i^i  B
)  \/  x  e.  ( A  i^i  C
) ) )
6 elun 3329 . . . 4  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
76anbi2i 675 . . 3  |-  ( ( x  e.  A  /\  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  /\  (
x  e.  B  \/  x  e.  C )
) )
8 elun 3329 . . 3  |-  ( x  e.  ( ( A  i^i  B )  u.  ( A  i^i  C
) )  <->  ( x  e.  ( A  i^i  B
)  \/  x  e.  ( A  i^i  C
) ) )
95, 7, 83bitr4i 268 . 2  |-  ( ( x  e.  A  /\  x  e.  ( B  u.  C ) )  <->  x  e.  ( ( A  i^i  B )  u.  ( A  i^i  C ) ) )
109ineqri 3375 1  |-  ( A  i^i  ( B  u.  C ) )  =  ( ( A  i^i  B )  u.  ( A  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    \/ wo 357    /\ wa 358    = wceq 1632    e. wcel 1696    u. cun 3163    i^i cin 3164
This theorem is referenced by:  indir  3430  difindi  3436  undisj2  3520  disjssun  3525  difdifdir  3554  diftpsn3  3772  resundi  4985  fresaun  5428  elfiun  7199  unxpwdom  7319  kmlem2  7793  cdainf  7834  ackbij1lem1  7862  ackbij1lem2  7863  ssxr  8908  incexclem  12311  bitsinv1  12649  bitsinvp1  12656  bitsres  12680  paste  17038  unmbl  18911  ovolioo  18941  uniioombllem4  18957  volcn  18977  ellimc2  19243  lhop2  19378  ex-in  20828  hdrmp  25809  disjpr2  28185
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172
  Copyright terms: Public domain W3C validator