Theorem dfrn2

Description: Alternate definition of range. Definition 4 of Suppes p. 60. (Contributed by NM, 27-Dec-1996)

	Ref	Expression
Assertion	dfrn2	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
2		df-dm	⊢ dom ◡ 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑦 ◡ 𝐴 𝑥 }
3		vex	⊢ 𝑦 ∈ V
4		vex	⊢ 𝑥 ∈ V
5	3 4	brcnv	⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
6	5	exbii	⊢ ( ∃ 𝑥 𝑦 ◡ 𝐴 𝑥 ↔ ∃ 𝑥 𝑥 𝐴 𝑦 )
7	6	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 ◡ 𝐴 𝑥 } = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }
8	1 2 7	3eqtri	⊢ ran 𝐴 = { 𝑦 ∣ ∃ 𝑥 𝑥 𝐴 𝑦 }