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

Theorem iunin2 4119
Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4108 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 2826 . . . 4  |-  ( E. x  e.  A  ( y  e.  B  /\  y  e.  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
2 elin 3494 . . . . 5  |-  ( y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e.  C ) )
32rexbii 2695 . . . 4  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  E. x  e.  A  ( y  e.  B  /\  y  e.  C
) )
4 eliun 4061 . . . . 5  |-  ( y  e.  U_ x  e.  A  C  <->  E. x  e.  A  y  e.  C )
54anbi2i 676 . . . 4  |-  ( ( y  e.  B  /\  y  e.  U_ x  e.  A  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
61, 3, 53bitr4i 269 . . 3  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
7 eliun 4061 . . 3  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  E. x  e.  A  y  e.  ( B  i^i  C ) )
8 elin 3494 . . 3  |-  ( y  e.  ( B  i^i  U_ x  e.  A  C
)  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
96, 7, 83bitr4i 269 . 2  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  y  e.  ( B  i^i  U_ x  e.  A  C )
)
109eqriv 2405 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 359    = wceq 1649    e. wcel 1721   E.wrex 2671    i^i cin 3283   U_ciun 4057
This theorem is referenced by:  iunin1  4120  2iunin  4123  resiun1  5128  resiun2  5129  kmlem11  8000  cmpsublem  17420  cmpsub  17421  kgentopon  17527  metnrmlem3  18848  ovoliunlem1  19355  voliunlem1  19401  voliunlem2  19402  uniioombllem2  19432  uniioombllem4  19435  volsup2  19454  itg1addlem5  19549  itg1climres  19563  cvmscld  24917  cnambfre  26158  heiborlem3  26416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ral 2675  df-rex 2676  df-v 2922  df-in 3291  df-iun 4059
  Copyright terms: Public domain W3C validator