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

Theorem iunin2 4394
 Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 4383 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
Assertion
Ref Expression
iunin2
Distinct variable group:   ,

Proof of Theorem iunin2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 r19.42v 3012 . . . 4
2 elin 3686 . . . . 5
32rexbii 2959 . . . 4
4 eliun 4335 . . . . 5
54anbi2i 694 . . . 4
61, 3, 53bitr4i 277 . . 3
7 eliun 4335 . . 3
8 elin 3686 . . 3
96, 7, 83bitr4i 277 . 2
109eqriv 2453 1
 Colors of variables: wff setvar class Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  E.wrex 2808  i^icin 3474  U_ciun 4330 This theorem is referenced by:  iunin1  4395  2iunin  4398  resiun1  5297  resiun2  5298  infssuni  7831  kmlem11  8561  cmpsublem  19899  cmpsub  19900  kgentopon  20039  metnrmlem3  21365  ovoliunlem1  21913  voliunlem1  21960  voliunlem2  21961  uniioombllem2  21992  uniioombllem4  21995  volsup2  22014  itg1addlem5  22107  itg1climres  22121  cvmscld  28718  cnambfre  30063  ftc1anclem6  30095  heiborlem3  30309 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-iun 4332
 Copyright terms: Public domain W3C validator