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 ) |