Metamath Proof Explorer


Theorem fvn0fvelrn

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 )

Proof

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 )