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

Theorem iunxun 4982
 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 4120 . . . 4 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
2 eliun 4888 . . . . 5 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
3 eliun 4888 . . . . 5 (𝑦 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑦𝐶)
42, 3orbi12i 912 . . . 4 ((𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶) ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
51, 4bitr4i 281 . . 3 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
6 eliun 4888 . . 3 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴𝐵)𝑦𝐶)
7 elun 4079 . . 3 (𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶) ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
85, 6, 73bitr4i 306 . 2 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶))
98eqriv 2798 1 𝑥 ∈ (𝐴𝐵)𝐶 = ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 844   = wceq 1538   ∈ wcel 2112  ∃wrex 3110   ∪ cun 3882  ∪ ciun 4884 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-un 3889  df-iun 4886 This theorem is referenced by:  iunxdif3  4983  iunxprg  4984  iunsuc  6245  funiunfv  6989  iunfi  8800  kmlem11  9575  ackbij1lem9  9643  fsum2dlem  15120  fsumiun  15171  fprod2dlem  15329  prmreclem4  16248  fiuncmp  22012  ovolfiniun  24108  finiunmbl  24151  volfiniun  24154  voliunlem1  24157  uniioombllem4  24193  iuninc  30327  iunxunsn  30333  iunxunpr  30334  ofpreima2  30432  indval2  31381  esum2dlem  31459  sigaclfu2  31488  fiunelros  31541  measvuni  31581  cvmliftlem10  32649  mrsubvrs  32877  mblfinlem2  35088  dfrcl4  40364  iunrelexp0  40390  comptiunov2i  40394  corclrcl  40395  trclfvdecomr  40416  dfrtrcl4  40426  corcltrcl  40427  cotrclrcl  40430  fiiuncl  41686  iunp1  41687  sge0iunmptlemfi  43039  ovolval4lem1  43275
 Copyright terms: Public domain W3C validator