Theorem rniun

Description: The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015)

	Ref	Expression
Assertion	rniun	⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵

Proof

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