Theorem dfrn3

Description: Alternate definition of range. Definition 6.5(2) of TakeutiZaring p. 24. (Contributed by NM, 28-Dec-1996)

	Ref	Expression
Assertion	dfrn3	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		dfrn2	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }
2		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3	2	exbii	⊢ ( ∃ 𝑥 𝑥 𝐴 𝑦 ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
4	3	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 } = { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }
5	1 4	eqtri	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }