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

Theorem iunin2 3967
Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 3956 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
StepHypRef Expression
1 r19.42v 2695 . . . 4  |-  ( E. x  e.  A  ( y  e.  B  /\  y  e.  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
2 elin 3359 . . . . 5  |-  ( y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e.  C ) )
32rexbii 2569 . . . 4  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  E. x  e.  A  ( y  e.  B  /\  y  e.  C
) )
4 eliun 3910 . . . . 5  |-  ( y  e.  U_ x  e.  A  C  <->  E. x  e.  A  y  e.  C )
54anbi2i 678 . . . 4  |-  ( ( y  e.  B  /\  y  e.  U_ x  e.  A  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
61, 3, 53bitr4i 270 . . 3  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
7 eliun 3910 . . 3  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  E. x  e.  A  y  e.  ( B  i^i  C ) )
8 elin 3359 . . 3  |-  ( y  e.  ( B  i^i  U_ x  e.  A  C
)  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
96, 7, 83bitr4i 270 . 2  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  y  e.  ( B  i^i  U_ x  e.  A  C )
)
109eqriv 2281 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 360    = wceq 1628    e. wcel 1688   E.wrex 2545    i^i cin 3152   U_ciun 3906
This theorem is referenced by:  iunin1  3968  2iunin  3971  resiundiOLD  4744  resiun1  4973  resiun2  4974  kmlem11  7781  cmpsublem  17120  cmpsub  17121  kgentopon  17227  metnrmlem3  18359  ovoliunlem1  18855  voliunlem1  18901  voliunlem2  18902  uniioombllem2  18932  uniioombllem4  18935  volsup2  18954  itg1addlem5  19049  itg1climres  19063  cvmscld  23208  isunscov  24472  heiborlem3  25936
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ral 2549  df-rex 2550  df-v 2791  df-in 3160  df-iun 3908
  Copyright terms: Public domain W3C validator