Metamath Proof Explorer

Theorem cnvresrn

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

Ref Expression
Assertion cnvresrn 
|- ( `' R |` ran R ) = `' R

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran R = dom `' R
2 1 reseq2i 
 |-  ( `' R |` ran R ) = ( `' R |` dom `' R )
3 relcnv 
 |-  Rel `' R
4 dfrel5 
 |-  ( Rel `' R <-> ( `' R |` dom `' R ) = `' R )
5 3 4 mpbi 
 |-  ( `' R |` dom `' R ) = `' R
6 2 5 eqtri 
 |-  ( `' R |` ran R ) = `' R