This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ dom ⁡ F ∧ Y ∉ ran ⁡ F → F ⁡ X ≠ Y

Proof

Step Hyp Ref Expression
1 fvelrn ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F → F ⁡ X ∈ ran ⁡ F
2 elnelne2 ⊢ F ⁡ X ∈ ran ⁡ F ∧ Y ∉ ran ⁡ F → F ⁡ X ≠ Y
3 1 2 stoic3 ⊢ Fun ⁡ F ∧ X ∈ dom ⁡ F ∧ Y ∉ ran ⁡ F → F ⁡ X ≠ Y