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 𝐵