Theorem dfrn4

Description: Range defined in terms of image. (Contributed by NM, 14-May-2008)

	Ref	Expression
Assertion	dfrn4	$$⊢\mathrm{ran}A=A\left[\mathrm{V}\right]$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢A\left[\mathrm{V}\right]=\mathrm{ran}\left({A\upharpoonright }_{\mathrm{V}}\right)$$
2		rnresv	$$⊢\mathrm{ran}\left({A\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}A$$
3	1 2	eqtr2i	$$⊢\mathrm{ran}A=A\left[\mathrm{V}\right]$$