Description: The preimage of a superset of the range of a class is equal to the domain of the class. Generalization of cnvimarndm to supersets of the range. (Contributed by AV, 18-Sep-2024) (Proof shortened by BJ, 29-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvimassrndm | |- ( ran F C_ A -> ( `' F " A ) = dom F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfdm4 | |- dom F = ran `' F |
|
| 2 | df-rn | |- ran F = dom `' F |
|
| 3 | 2 | sseq1i | |- ( ran F C_ A <-> dom `' F C_ A ) |
| 4 | dfrn7 | |- ( dom `' F C_ A -> ran `' F = ( `' F " A ) ) |
|
| 5 | 3 4 | sylbi | |- ( ran F C_ A -> ran `' F = ( `' F " A ) ) |
| 6 | 1 5 | eqtr2id | |- ( ran F C_ A -> ( `' F " A ) = dom F ) |