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 \land X \in dom F \land Y \notin ran F) \to F (X) \neq Y$

Step	Hyp	Ref	Expression
1		fvelrn	$⊢ (Fun F \land X \in dom F) \to F (X) \in ran F$
2		elnelne2	$⊢ (F (X) \in ran F \land Y \notin ran F) \to F (X) \neq Y$
3	1 2	stoic3	$⊢ (Fun F \land X \in dom F \land Y \notin ran F) \to F (X) \neq Y$