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 𝐹 ∧ 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∉ ran 𝐹 ) → ( 𝐹 ‘ 𝑋 ) ≠ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 )
2		elnelne2	⊢ ( ( ( 𝐹 ‘ 𝑋 ) ∈ ran 𝐹 ∧ 𝑌 ∉ ran 𝐹 ) → ( 𝐹 ‘ 𝑋 ) ≠ 𝑌 )
3	1 2	stoic3	⊢ ( ( Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹 ∧ 𝑌 ∉ ran 𝐹 ) → ( 𝐹 ‘ 𝑋 ) ≠ 𝑌 )