Theorem bj-cnvresrn

Description: Duplicate of cnvresrn , to be moved to the main section. The converse restricted to the range is equal to the converse. Analogue of resdmb since a converse is always a relation ( relcnv ). (Contributed by Peter Mazsa, 3-Sep-2021) Can shorten domss2 .

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

Proof

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