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

Metamath Proof Explorer

Theorem dmiun

Description: The domain of an indexed union. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Assertion dmiun dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 )
2 vex ⊢ 𝑦 ∈ V
3 2 eldm2 ⊢ ( 𝑦 ∈ dom 𝐵 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 )
4 3 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 )
5 eliun ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 )
6 5 exbii ⊢ ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 )
7 1 4 6 3bitr4ri ⊢ ( ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝐵 )
8 2 eldm2 ⊢ ( 𝑦 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑧 ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
9 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝐵 )
10 7 8 9 3bitr4i ⊢ ( 𝑦 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 dom 𝐵 )
11 10 eqriv ⊢ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 dom 𝐵