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

Theorem iunin2 5075
Description: Indexed union of intersection. Generalization of half of theorem "Distributive laws" in [Enderton] p. 30. Use uniiun 5062 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 3188 . . . 4 (∃𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝑦𝐶))
2 elin 3978 . . . . 5 (𝑦 ∈ (𝐵𝐶) ↔ (𝑦𝐵𝑦𝐶))
32rexbii 3091 . . . 4 (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ ∃𝑥𝐴 (𝑦𝐵𝑦𝐶))
4 eliun 4999 . . . . 5 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
54anbi2i 623 . . . 4 ((𝑦𝐵𝑦 𝑥𝐴 𝐶) ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝑦𝐶))
61, 3, 53bitr4i 303 . . 3 (∃𝑥𝐴 𝑦 ∈ (𝐵𝐶) ↔ (𝑦𝐵𝑦 𝑥𝐴 𝐶))
7 eliun 4999 . . 3 (𝑦 𝑥𝐴 (𝐵𝐶) ↔ ∃𝑥𝐴 𝑦 ∈ (𝐵𝐶))
8 elin 3978 . . 3 (𝑦 ∈ (𝐵 𝑥𝐴 𝐶) ↔ (𝑦𝐵𝑦 𝑥𝐴 𝐶))
96, 7, 83bitr4i 303 . 2 (𝑦 𝑥𝐴 (𝐵𝐶) ↔ 𝑦 ∈ (𝐵 𝑥𝐴 𝐶))
109eqriv 2731 1 𝑥𝐴 (𝐵𝐶) = (𝐵 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1536  wcel 2105  wrex 3067  cin 3961   ciun 4995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-v 3479  df-in 3969  df-iun 4997
This theorem is referenced by:  iunin1  5076  2iunin  5080  resiun2  6020  infssuni  9383  kmlem11  10198  cmpsublem  23422  cmpsub  23423  kgentopon  23561  metnrmlem3  24896  ovoliunlem1  25550  voliunlem1  25598  voliunlem2  25599  uniioombllem2  25631  uniioombllem4  25634  volsup2  25653  itg1addlem5  25749  itg1climres  25763  uniin2  32572  carsgclctunlem2  34300  cvmscld  35257  cnambfre  37654  ftc1anclem6  37684  heiborlem3  37799  carageniuncllem2  46477
  Copyright terms: Public domain W3C validator