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	|- ran `' `' A = ran A

Proof

Step	Hyp	Ref	Expression
1		df-rn	|- ran A = dom `' A
2		dfdm4	|- dom `' A = ran `' `' A
3	1 2	eqtr2i	|- ran `' `' A = ran A