Theorem iunxiun

Description: Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016)

	Ref	Expression
Assertion	iunxiun	⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶

Proof

Step	Hyp	Ref	Expression
1		eliun	⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝐵 )
2	1	anbi1i	⊢ ( ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
3		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
4	2 3	bitr4i	⊢ ( ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
5	4	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
6		rexcom4	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
7	5 6	bitr4i	⊢ ( ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
8		df-rex	⊢ ( ∃ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝑧 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
9		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑧 ∈ 𝐶 )
10		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐵 𝑧 ∈ 𝐶 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
11	9 10	bitri	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
12	11	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
13	7 8 12	3bitr4i	⊢ ( ∃ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝑧 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 )
14		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ↔ ∃ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝑧 ∈ 𝐶 )
15		eliun	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 )
16	13 14 15	3bitr4i	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 )
17	16	eqriv	⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶