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

Theorem iunin2 4356
Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4345 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 2957 . . . 4  |-  ( E. x  e.  A  ( y  e.  B  /\  y  e.  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
2 elin 3629 . . . . 5  |-  ( y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e.  C ) )
32rexbii 2901 . . . 4  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  E. x  e.  A  ( y  e.  B  /\  y  e.  C
) )
4 eliun 4297 . . . . 5  |-  ( y  e.  U_ x  e.  A  C  <->  E. x  e.  A  y  e.  C )
54anbi2i 705 . . . 4  |-  ( ( y  e.  B  /\  y  e.  U_ x  e.  A  C )  <->  ( y  e.  B  /\  E. x  e.  A  y  e.  C ) )
61, 3, 53bitr4i 285 . . 3  |-  ( E. x  e.  A  y  e.  ( B  i^i  C )  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
7 eliun 4297 . . 3  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  E. x  e.  A  y  e.  ( B  i^i  C ) )
8 elin 3629 . . 3  |-  ( y  e.  ( B  i^i  U_ x  e.  A  C
)  <->  ( y  e.  B  /\  y  e. 
U_ x  e.  A  C ) )
96, 7, 83bitr4i 285 . 2  |-  ( y  e.  U_ x  e.  A  ( B  i^i  C )  <->  y  e.  ( B  i^i  U_ x  e.  A  C )
)
109eqriv 2459 1  |-  U_ x  e.  A  ( B  i^i  C )  =  ( B  i^i  U_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 375    = wceq 1455    e. wcel 1898   E.wrex 2750    i^i cin 3415   U_ciun 4292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-v 3059  df-in 3423  df-iun 4294
This theorem is referenced by:  iunin1  4357  2iunin  4360  resiun1  5145  resiun2  5146  infssuni  7896  kmlem11  8621  cmpsublem  20469  cmpsub  20470  kgentopon  20608  metnrmlem3  21933  metnrmlem3OLD  21948  ovoliunlem1  22510  voliunlem1  22559  voliunlem2  22560  uniioombllem2  22596  uniioombllem2OLD  22597  uniioombllem4  22600  volsup2  22619  itg1addlem5  22714  itg1climres  22728  uniin2  28220  carsgclctunlem2  29201  cvmscld  30046  cnambfre  32035  ftc1anclem6  32068  heiborlem3  32191  carageniuncllem2  38451
  Copyright terms: Public domain W3C validator