Description: The preimage of the codomain of a function is the function's domain. (Contributed by FL, 25-Jan-2007) (Proof shortened by AV, 20-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fimacnv | |- ( F : A --> B -> ( `' F " B ) = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frn | |- ( F : A --> B -> ran F C_ B ) |
|
| 2 | cnvimassrndm | |- ( ran F C_ B -> ( `' F " B ) = dom F ) |
|
| 3 | 1 2 | syl | |- ( F : A --> B -> ( `' F " B ) = dom F ) |
| 4 | fdm | |- ( F : A --> B -> dom F = A ) |
|
| 5 | 3 4 | eqtrd | |- ( F : A --> B -> ( `' F " B ) = A ) |