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 | |- ( `' R |` ran R ) = `' R |
| 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 | resdmb | |- ( Rel `' R <-> ( `' R |` dom `' R ) = `' R ) |
|
| 5 | 3 4 | mpbi | |- ( `' R |` dom `' R ) = `' R |
| 6 | 2 5 | eqtri | |- ( `' R |` ran R ) = `' R |