Metamath Proof Explorer

Theorem nelrnfvne

Description: A function value cannot be any element not contained in the range of the function. (Contributed by AV, 28-Jan-2020)

Ref Expression
Assertion nelrnfvne 
|- ( ( Fun F /\ X e. dom F /\ Y e/ ran F ) -> ( F ` X ) =/= Y )

Proof

Step Hyp Ref Expression
1 fvelrn 
 |-  ( ( Fun F /\ X e. dom F ) -> ( F ` X ) e. ran F )
2 elnelne2 
 |-  ( ( ( F ` X ) e. ran F /\ Y e/ ran F ) -> ( F ` X ) =/= Y )
3 1 2 stoic3 
 |-  ( ( Fun F /\ X e. dom F /\ Y e/ ran F ) -> ( F ` X ) =/= Y )