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

Theorem iunin2 5071
Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5058 to recover Enderton's theorem. (Contributed by NM, 26-Mar-2004.)
Assertion
Ref Expression
iunin2 𝑥𝐴 (𝐵𝐶) = (𝐵 𝑥𝐴 𝐶)
Distinct variable group:   𝑥,𝐵
Allowed substitution hints:   𝐴(𝑥)   𝐶(𝑥)

Proof of Theorem iunin2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 r19.42v 3191 . . . 4 (∃𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝑦𝐶))
2 elin 3967 . . . . 5 (𝑦 ∈ (𝐵𝐶) ↔ (𝑦𝐵𝑦𝐶))
32rexbii 3094 . . . 4 (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ ∃𝑥𝐴 (𝑦𝐵𝑦𝐶))
4 eliun 4995 . . . . 5 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
54anbi2i 623 . . . 4 ((𝑦𝐵𝑦 𝑥𝐴 𝐶) ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝑦𝐶))
61, 3, 53bitr4i 303 . . 3 (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (𝑦𝐵𝑦 𝑥𝐴 𝐶))
7 eliun 4995 . . 3 (𝑦 𝑥𝐴 (𝐵𝐶) ↔ ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
8 elin 3967 . . 3 (𝑦 ∈ (𝐵 𝑥𝐴 𝐶) ↔ (𝑦𝐵𝑦 𝑥𝐴 𝐶))
96, 7, 83bitr4i 303 . 2 (𝑦 𝑥𝐴 (𝐵𝐶) ↔ 𝑦 ∈ (𝐵 𝑥𝐴 𝐶))
109eqriv 2734 1 𝑥𝐴 (𝐵𝐶) = (𝐵 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wcel 2108  wrex 3070  cin 3950   ciun 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-in 3958  df-iun 4993
This theorem is referenced by:  iunin1  5072  2iunin  5076  resiun2  6018  infssuni  9386  kmlem11  10201  cmpsublem  23407  cmpsub  23408  kgentopon  23546  metnrmlem3  24883  ovoliunlem1  25537  voliunlem1  25585  voliunlem2  25586  uniioombllem2  25618  uniioombllem4  25621  volsup2  25640  itg1addlem5  25735  itg1climres  25749  uniin2  32565  carsgclctunlem2  34321  cvmscld  35278  cnambfre  37675  ftc1anclem6  37705  heiborlem3  37820  carageniuncllem2  46537
  Copyright terms: Public domain W3C validator