Theorem rncnvcnv

Description: The range of the double converse of a class is equal to its range (even when that class in not a relation). (Contributed by NM, 8-Apr-2007)

	Ref	Expression
Assertion	rncnvcnv	$$⊢\mathrm{ran}{A^{-1}}^{-1}=\mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
2		dfdm4	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}{A^{-1}}^{-1}$$
3	1 2	eqtr2i	$$⊢\mathrm{ran}{A^{-1}}^{-1}=\mathrm{ran}A$$