Description: If a function value has a member, then the argument belongs to the domain. (An artifact of our function value definition.) (Contributed by NM, 12-Feb-2007) (Proof shortened by BJ, 22-Oct-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elfvdm | |- ( A e. ( F ` B ) -> B e. dom F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | n0i | |- ( A e. ( F ` B ) -> -. ( F ` B ) = (/) ) |
|
| 2 | ndmfv | |- ( -. B e. dom F -> ( F ` B ) = (/) ) |
|
| 3 | 1 2 | nsyl2 | |- ( A e. ( F ` B ) -> B e. dom F ) |