Theorem iunxun

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)

	Ref	Expression
Assertion	iunxun	⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = ( ∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rexun	⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝑦 ∈ 𝐶 ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ) )
2		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 )
3		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 )
4	2 3	orbi12i	⊢ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ∨ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ) )
5	1 4	bitr4i	⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝑦 ∈ 𝐶 ↔ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ) )
6		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 ↔ ∃ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝑦 ∈ 𝐶 )
7		elun	⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶 ) ↔ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ∨ 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ) )
8	5 6 7	3bitr4i	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 ↔ 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶 ) )
9	8	eqriv	⊢ ∪ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝐶 = ( ∪ 𝑥 ∈ 𝐴 𝐶 ∪ ∪ 𝑥 ∈ 𝐵 𝐶 )