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	$$⊢\mathrm{ran}A=\left\{y|\exists x⟨x,y⟩\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfrn2	$$⊢\mathrm{ran}A=\left\{y|\exists xxAy\right\}$$
2		df-br	$$⊢xAy\leftrightarrow ⟨x,y⟩\in A$$
3	2	exbii	$$⊢\exists xxAy\leftrightarrow \exists x⟨x,y⟩\in A$$
4	3	abbii	$$⊢\left\{y|\exists xxAy\right\}=\left\{y|\exists x⟨x,y⟩\in A\right\}$$
5	1 4	eqtri	$$⊢\mathrm{ran}A=\left\{y|\exists x⟨x,y⟩\in A\right\}$$