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 ◡ ◡ 𝐴 = ran 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
2		dfdm4	⊢ dom ◡ 𝐴 = ran ◡ ◡ 𝐴
3	1 2	eqtr2i	⊢ ran ◡ ◡ 𝐴 = ran 𝐴