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

Theorem iunxun 5098
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 4205 . . . 4 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
2 eliun 4999 . . . . 5 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
3 eliun 4999 . . . . 5 (𝑦 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑦𝐶)
42, 3orbi12i 914 . . . 4 ((𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶) ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
51, 4bitr4i 278 . . 3 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
6 eliun 4999 . . 3 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴𝐵)𝑦𝐶)
7 elun 4162 . . 3 (𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶) ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
85, 6, 73bitr4i 303 . 2 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶))
98eqriv 2731 1 𝑥 ∈ (𝐴𝐵)𝐶 = ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wo 847   = wceq 1536  wcel 2105  wrex 3067  cun 3960   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-or 848  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-un 3967  df-iun 4997
This theorem is referenced by:  iunxdif3  5099  iunxprg  5100  iunsuc  6470  funiunfv  7267  iunfi  9380  kmlem11  10198  ackbij1lem9  10264  fsum2dlem  15802  fsumiun  15853  fprod2dlem  16012  prmreclem4  16952  fiuncmp  23427  ovolfiniun  25549  finiunmbl  25592  volfiniun  25595  voliunlem1  25598  uniioombllem4  25634  iuninc  32580  iunxunsn  32586  iunxunpr  32587  ofpreima2  32682  indval2  33994  esum2dlem  34072  sigaclfu2  34101  fiunelros  34154  measvuni  34194  cvmliftlem10  35278  mrsubvrs  35506  mblfinlem2  37644  dfrcl4  43665  iunrelexp0  43691  comptiunov2i  43695  corclrcl  43696  trclfvdecomr  43717  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731  fiiuncl  45004  iunp1  45005  sge0iunmptlemfi  46368  ovolval4lem1  46604
  Copyright terms: Public domain W3C validator