Metamath Proof Explorer


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 𝑅 ) = 𝑅