Theorem cnvresrn

Description: Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021)

	Ref	Expression
Assertion	cnvresrn	⊢ ( ◡ 𝑅 ↾ ran 𝑅 ) = ◡ 𝑅

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝑅 = dom ◡ 𝑅
2	1	reseq2i	⊢ ( ◡ 𝑅 ↾ ran 𝑅 ) = ( ◡ 𝑅 ↾ dom ◡ 𝑅 )
3		relcnv	⊢ Rel ◡ 𝑅
4		dfrel5	⊢ ( Rel ◡ 𝑅 ↔ ( ◡ 𝑅 ↾ dom ◡ 𝑅 ) = ◡ 𝑅 )
5	3 4	mpbi	⊢ ( ◡ 𝑅 ↾ dom ◡ 𝑅 ) = ◡ 𝑅
6	2 5	eqtri	⊢ ( ◡ 𝑅 ↾ ran 𝑅 ) = ◡ 𝑅