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

Metamath Proof Explorer

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