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.

Step	Hyp	Ref	Expression
1		rexun 4188	. . . 4 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
2		eliun 5001	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
3		eliun 5001	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)
4	2, 3	orbi12i 912	. . . 4 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
5	1, 4	bitr4i 277	. . 3 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
6		eliun 5001	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶)
7		elun 4145	. . 3 ⊢ (𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
8	5, 6, 7	3bitr4i 302	. 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ 𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶))
9	8	eqriv 2722	1 ⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   ∨ wo 845   = wceq 1533   ∈ wcel 2098  ∃wrex 3059   ∪ cun 3942  ∪ ciun 4997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rex 3060  df-v 3463  df-un 3949  df-iun 4999

This theorem is referenced by:  iunxdif3  5099  iunxprg  5100  iunsuc  6456  funiunfv  7258  iunfi  9371  kmlem11  10190  ackbij1lem9  10258  fsum2dlem  15760  fsumiun  15811  fprod2dlem  15968  prmreclem4  16907  fiuncmp  23369  ovolfiniun  25491  finiunmbl  25534  volfiniun  25537  voliunlem1  25540  uniioombllem4  25576  iuninc  32450  iunxunsn  32456  iunxunpr  32457  ofpreima2  32553  indval2  33784  esum2dlem  33862  sigaclfu2  33891  fiunelros  33944  measvuni  33984  cvmliftlem10  35055  mrsubvrs  35283  mblfinlem2  37282  dfrcl4  43253  iunrelexp0  43279  comptiunov2i  43283  corclrcl  43284  trclfvdecomr  43305  dfrtrcl4  43315  corcltrcl  43316  cotrclrcl  43319  fiiuncl  44576  iunp1  44577  sge0iunmptlemfi  45944  ovolval4lem1  46180