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	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to F\left(X\right)\ne F\left(Y\right)$$

Proof

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