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

Theorem indi 3322
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
StepHypRef Expression
1 andi 842 . . . 4  |-  ( ( x  e.  A  /\  ( x  e.  B  \/  x  e.  C
) )  <->  ( (
x  e.  A  /\  x  e.  B )  \/  ( x  e.  A  /\  x  e.  C
) ) )
2 elin 3266 . . . . 5  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3266 . . . . 5  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
42, 3orbi12i 509 . . . 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 245 . . 3  |-  ( ( x  e.  A  /\  ( x  e.  B  \/  x  e.  C
) )  <->  ( x  e.  ( A  i^i  B
)  \/  x  e.  ( A  i^i  C
) ) )
6 elun 3226 . . . 4  |-  ( x  e.  ( B  u.  C )  <->  ( x  e.  B  \/  x  e.  C ) )
76anbi2i 678 . . 3  |-  ( ( x  e.  A  /\  x  e.  ( B  u.  C ) )  <->  ( x  e.  A  /\  (
x  e.  B  \/  x  e.  C )
) )
8 elun 3226 . . 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 270 . 2  |-  ( ( x  e.  A  /\  x  e.  ( B  u.  C ) )  <->  x  e.  ( ( A  i^i  B )  u.  ( A  i^i  C ) ) )
109ineqri 3270 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 359    /\ wa 360    = wceq 1619    e. wcel 1621    u. cun 3076    i^i cin 3077
This theorem is referenced by:  indir  3324  difindi  3330  undisj2  3414  disjssun  3419  difdifdir  3447  resundi  4876  fresaun  5269  elfiun  7067  unxpwdom  7187  kmlem2  7661  cdainf  7702  ackbij1lem1  7730  ackbij1lem2  7731  ssxr  8772  bitsinv1  12507  bitsinvp1  12514  bitsres  12538  paste  16854  unmbl  18727  ovolioo  18757  uniioombllem4  18773  volcn  18793  ellimc2  19059  lhop2  19194  ex-in  20625  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