Theorem dfrn2

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

	Ref	Expression
Assertion	dfrn2	$$⊢\mathrm{ran}A=\left\{y|\exists xxAy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
2		df-dm	$$⊢\mathrm{dom}{A}^{-1}=\left\{y|\exists xy{A}^{-1}x\right\}$$
3		vex	$$⊢y\in \mathrm{V}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	3 4	brcnv	$$⊢y{A}^{-1}x\leftrightarrow xAy$$
6	5	exbii	$$⊢\exists xy{A}^{-1}x\leftrightarrow \exists xxAy$$
7	6	abbii	$$⊢\left\{y|\exists xy{A}^{-1}x\right\}=\left\{y|\exists xxAy\right\}$$
8	1 2 7	3eqtri	$$⊢\mathrm{ran}A=\left\{y|\exists xxAy\right\}$$