Description: If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Proof shortened by SN, 13-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fvn0fvelrn | |- ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvrn0 | |- ( F ` X ) e. ( ran F u. { (/) } ) |
|
| 2 | nelsn | |- ( ( F ` X ) =/= (/) -> -. ( F ` X ) e. { (/) } ) |
|
| 3 | elunnel2 | |- ( ( ( F ` X ) e. ( ran F u. { (/) } ) /\ -. ( F ` X ) e. { (/) } ) -> ( F ` X ) e. ran F ) |
|
| 4 | 1 2 3 | sylancr | |- ( ( F ` X ) =/= (/) -> ( F ` X ) e. ran F ) |