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

Metamath Proof Explorer

Theorem iuncom4

Description: Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014)

Ref Expression
Assertion iuncom4 ∪ 𝑥 ∈ 𝐴 ∪ 𝐵 = ∪ ∪ 𝑥 ∈ 𝐴 𝐵

Proof

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