Theorem rnresv

Description: The range of a universal restriction. (Contributed by NM, 14-May-2008)

	Ref	Expression
Assertion	rnresv	$$⊢\mathrm{ran}\left({A\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	$$⊢{A^{-1}}^{-1}={A\upharpoonright }_{\mathrm{V}}$$
2	1	rneqi	$$⊢\mathrm{ran}{A^{-1}}^{-1}=\mathrm{ran}\left({A\upharpoonright }_{\mathrm{V}}\right)$$
3		rncnvcnv	$$⊢\mathrm{ran}{A^{-1}}^{-1}=\mathrm{ran}A$$
4	2 3	eqtr3i	$$⊢\mathrm{ran}\left({A\upharpoonright }_{\mathrm{V}}\right)=\mathrm{ran}A$$