Theorem iunxun 5062

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 4155	. . . 4 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
2		eliun 4962	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶)
3		eliun 4962	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶)
4	2, 3	orbi12i 927	. . . 4 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶))
5	1, 4	bitr4i 281	. . 3 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶 ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
6		eliun 4962	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ ∃𝑥 ∈ (𝐴 ∪ 𝐵)𝑦 ∈ 𝐶)
7		elun 4113	. . 3 ⊢ (𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶) ↔ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶))
8	5, 6, 7	3bitr4i 306	. 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ 𝑦 ∈ (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶))
9	8	eqriv 2766	1 ⊢ ∪ 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 = (∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   ∨ wo 860   = wceq 1567   ∈ wcel 2149  ∃wrex 3095   ∪ cun 3909  ∪ ciun 4958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-v 3463  df-un 3916  df-iun 4960

This theorem is referenced by:  iunxdif3  5063  iunxprg  5064  iunsuc  6449  funiunfv  7247  iunfi  9300  kmlem11  10144  ackbij1lem9  10210  indval2  12223  fsum2dlem  15821  fsumiun  15873  fprod2dlem  16034  prmreclem4  16979  fiuncmp  23530  ovolfiniun  25629  finiunmbl  25672  volfiniun  25675  voliunlem1  25678  uniioombllem4  25714  iuninc  32846  iunxunsn  32852  iunxunpr  32853  ofpreima2  32952  esum2dlem  34427  sigaclfu2  34456  fiunelros  34509  measvuni  34549  cvmliftlem10  35719  mrsubvrs  35947  ttcun  36946  mblfinlem2  38232  dfrcl4  44329  iunrelexp0  44355  comptiunov2i  44359  corclrcl  44360  trclfvdecomr  44381  dfrtrcl4  44391  corcltrcl  44392  cotrclrcl  44395  fiiuncl  45712  iunp1  45713  sge0iunmptlemfi  47054  ovolval4lem1  47290