Theorem iunxun 5040

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 4143	. . . 4 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
2		eliun 4943	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
3		eliun 4943	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)
4	2, 3	orbi12i 914	. . . 4 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
5	1, 4	bitr4i 278	. . 3 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
6		eliun 4943	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶)
7		elun 4100	. . 3 ⊢ (𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
8	5, 6, 7	3bitr4i 303	. 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ 𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶))
9	8	eqriv 2728	1 ⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2111  ∃wrex 3056   ∪ cun 3895  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-v 3438  df-un 3902  df-iun 4941

This theorem is referenced by:  iunxdif3  5041  iunxprg  5042  iunsuc  6393  funiunfv  7182  iunfi  9227  kmlem11  10052  ackbij1lem9  10118  fsum2dlem  15677  fsumiun  15728  fprod2dlem  15887  prmreclem4  16831  fiuncmp  23319  ovolfiniun  25429  finiunmbl  25472  volfiniun  25475  voliunlem1  25478  uniioombllem4  25514  iuninc  32540  iunxunsn  32546  iunxunpr  32547  ofpreima2  32648  indval2  32835  esum2dlem  34105  sigaclfu2  34134  fiunelros  34187  measvuni  34227  cvmliftlem10  35338  mrsubvrs  35566  mblfinlem2  37697  dfrcl4  43768  iunrelexp0  43794  comptiunov2i  43798  corclrcl  43799  trclfvdecomr  43820  dfrtrcl4  43830  corcltrcl  43831  cotrclrcl  43834  fiiuncl  45161  iunp1  45162  sge0iunmptlemfi  46510  ovolval4lem1  46746