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

Theorem iunxun 4541
 Description: Separate a union in the index of an indexed union. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)
Assertion
Ref Expression
iunxun 𝑥 ∈ (𝐴𝐵)𝐶 = ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶)

Proof of Theorem iunxun
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 rexun 3755 . . . 4 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
2 eliun 4460 . . . . 5 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
3 eliun 4460 . . . . 5 (𝑦 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑦𝐶)
42, 3orbi12i 542 . . . 4 ((𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶) ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
51, 4bitr4i 266 . . 3 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
6 eliun 4460 . . 3 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴𝐵)𝑦𝐶)
7 elun 3715 . . 3 (𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶) ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
85, 6, 73bitr4i 291 . 2 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶))
98eqriv 2607 1 𝑥 ∈ (𝐴𝐵)𝐶 = ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 382   = wceq 1475   ∈ wcel 1977  ∃wrex 2897   ∪ cun 3538  ∪ ciun 4455 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-un 3545  df-iun 4457 This theorem is referenced by:  iunxdif3  4542  iunxprg  4543  iunsuc  5724  funiunfv  6410  iunfi  8137  kmlem11  8865  ackbij1lem9  8933  fsum2dlem  14343  fsumiun  14394  fprod2dlem  14549  prmreclem4  15461  fiuncmp  21017  ovolfiniun  23076  finiunmbl  23119  volfiniun  23122  voliunlem1  23125  uniioombllem4  23160  iuninc  28761  ofpreima2  28849  indval2  29404  esum2dlem  29481  sigaclfu2  29511  fiunelros  29564  measvuni  29604  cvmliftlem10  30530  mrsubvrs  30673  mblfinlem2  32617  dfrcl4  36987  iunrelexp0  37013  comptiunov2i  37017  corclrcl  37018  trclfvdecomr  37039  dfrtrcl4  37049  corcltrcl  37050  cotrclrcl  37053  fiiuncl  38259  iunp1  38260  sge0iunmptlemfi  39306  ovolval4lem1  39539
 Copyright terms: Public domain W3C validator