This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvresrn

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

		Ref	Expression
	Assertion	cnvresrn	$⊢ {R^{-1} ↾}_{ran R} = R^{-1}$

Step	Hyp	Ref	Expression
1		df-rn	$⊢ ran R = dom R^{-1}$
2	1	reseq2i	$⊢ {R^{-1} ↾}_{ran R} = {R^{-1} ↾}_{dom R^{-1}}$
3		relcnv	$⊢ Rel R^{-1}$
4		dfrel5	$⊢ Rel R^{-1} \leftrightarrow {R^{-1} ↾}_{dom R^{-1}} = R^{-1}$
5	3 4	mpbi	$⊢ {R^{-1} ↾}_{dom R^{-1}} = R^{-1}$
6	2 5	eqtri	$⊢ {R^{-1} ↾}_{ran R} = R^{-1}$