Description: Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | cnvresrn | ⊢ ( ◡ 𝑅 ↾ ran 𝑅 ) = ◡ 𝑅 |
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 𝑅 ) = ◡ 𝑅 |