This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∪ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶