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

Theorem iunin2 3982
Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 3971 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
Assertion
Ref Expression
iunin2  |-  U_ x  e.  A  ( B  i^i  C )  =  ( B  i^i  U_ x  e.  A  C )
Distinct variable group:    x, B
Allowed substitution hints:    A( x)    C( x)

Proof of Theorem iunin2
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 r19.42v 2707 . . . 4  |-  ( E. x  e.  A  ( y  e.  B  /\  y  e.  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
2 elin 3371 . . . . 5  |-  ( y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e.  C ) )
32rexbii 2581 . . . 4  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  E. x  e.  A  ( y  e.  B  /\  y  e.  C
) )
4 eliun 3925 . . . . 5  |-  ( y  e.  U_ x  e.  A  C  <->  E. x  e.  A  y  e.  C )
54anbi2i 675 . . . 4  |-  ( ( y  e.  B  /\  y  e.  U_ x  e.  A  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
61, 3, 53bitr4i 268 . . 3  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
7 eliun 3925 . . 3  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  E. x  e.  A  y  e.  ( B  i^i  C ) )
8 elin 3371 . . 3  |-  ( y  e.  ( B  i^i  U_ x  e.  A  C
)  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
96, 7, 83bitr4i 268 . 2  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  y  e.  ( B  i^i  U_ x  e.  A  C )
)
109eqriv 2293 1  |-  U_ x  e.  A  ( B  i^i  C )  =  ( B  i^i  U_ x  e.  A  C )
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1632    e. wcel 1696   E.wrex 2557    i^i cin 3164   U_ciun 3921
This theorem is referenced by:  iunin1  3983  2iunin  3986  resiundiOLD  4761  resiun1  4990  resiun2  4991  kmlem11  7802  cmpsublem  17142  cmpsub  17143  kgentopon  17249  metnrmlem3  18381  ovoliunlem1  18877  voliunlem1  18923  voliunlem2  18924  uniioombllem2  18954  uniioombllem4  18957  volsup2  18976  itg1addlem5  19071  itg1climres  19085  cvmscld  23819  isunscov  25177  heiborlem3  26640
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-ral 2561  df-rex 2562  df-v 2803  df-in 3172  df-iun 3923
  Copyright terms: Public domain W3C validator