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

Theorem iunxun 5007
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 4163 . . . 4 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
2 eliun 4914 . . . . 5 (𝑦 𝑥𝐴 𝐶 ↔ ∃𝑥𝐴 𝑦𝐶)
3 eliun 4914 . . . . 5 (𝑦 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝑦𝐶)
42, 3orbi12i 908 . . . 4 ((𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶) ↔ (∃𝑥𝐴 𝑦𝐶 ∨ ∃𝑥𝐵 𝑦𝐶))
51, 4bitr4i 279 . . 3 (∃𝑥 ∈ (𝐴𝐵)𝑦𝐶 ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
6 eliun 4914 . . 3 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴𝐵)𝑦𝐶)
7 elun 4122 . . 3 (𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶) ↔ (𝑦 𝑥𝐴 𝐶𝑦 𝑥𝐵 𝐶))
85, 6, 73bitr4i 304 . 2 (𝑦 𝑥 ∈ (𝐴𝐵)𝐶𝑦 ∈ ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶))
98eqriv 2815 1 𝑥 ∈ (𝐴𝐵)𝐶 = ( 𝑥𝐴 𝐶 𝑥𝐵 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wo 841   = wceq 1528  wcel 2105  wrex 3136  cun 3931   ciun 4910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-v 3494  df-un 3938  df-iun 4912
This theorem is referenced by:  iunxdif3  5008  iunxprg  5009  iunsuc  6266  funiunfv  6998  iunfi  8800  kmlem11  9574  ackbij1lem9  9638  fsum2dlem  15113  fsumiun  15164  fprod2dlem  15322  prmreclem4  16243  fiuncmp  21940  ovolfiniun  24029  finiunmbl  24072  volfiniun  24075  voliunlem1  24078  uniioombllem4  24114  iuninc  30240  iunxunsn  30246  iunxunpr  30247  ofpreima2  30339  indval2  31172  esum2dlem  31250  sigaclfu2  31279  fiunelros  31332  measvuni  31372  cvmliftlem10  32438  mrsubvrs  32666  mblfinlem2  34811  dfrcl4  39899  iunrelexp0  39925  comptiunov2i  39929  corclrcl  39930  trclfvdecomr  39951  dfrtrcl4  39961  corcltrcl  39962  cotrclrcl  39965  fiiuncl  41204  iunp1  41205  sge0iunmptlemfi  42572  ovolval4lem1  42808
  Copyright terms: Public domain W3C validator