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

Metamath Proof Explorer

Theorem dff14i

Description: A one-to-one function maps different arguments onto different values. Implication of the alternate definition dff14a . (Contributed by AV, 30-Oct-2025)

		Ref	Expression
	Assertion	dff14i	$⊢ (F : A \underset{1-1}{⟶} B \land (X \in A \land Y \in A \land X \neq Y)) \to F (X) \neq F (Y)$

Proof

Step	Hyp	Ref	Expression
1		f1veqaeq	$⊢ (F : A \underset{1-1}{⟶} B \land (X \in A \land Y \in A)) \to (F (X) = F (Y) \to X = Y)$
2	1	necon3d	$⊢ (F : A \underset{1-1}{⟶} B \land (X \in A \land Y \in A)) \to (X \neq Y \to F (X) \neq F (Y))$
3	2	exp32	$⊢ F : A \underset{1-1}{⟶} B \to (X \in A \to (Y \in A \to (X \neq Y \to F (X) \neq F (Y))))$
4	3	3imp2	$⊢ (F : A \underset{1-1}{⟶} B \land (X \in A \land Y \in A \land X \neq Y)) \to F (X) \neq F (Y)$