Theorem dff15

Description: A one-to-one function in terms of different arguments never having the same function value. (Contributed by BTernaryTau, 24-Oct-2023)

	Ref	Expression
Assertion	dff15	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dff13	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
2		iman	$$⊢\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \left(F\left(x\right)=F\left(y\right)\wedge \neg x=y\right)$$
3		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
4	3	anbi2i	$$⊢\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\leftrightarrow \left(F\left(x\right)=F\left(y\right)\wedge \neg x=y\right)$$
5	2 4	xchbinxr	$$⊢\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
6	5	2ralbii	$$⊢\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\neg \left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
7		ralnex2	$$⊢\forall x\in A\forall y\in A\neg \left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\leftrightarrow \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
8	6 7	bitri	$$⊢\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
9	8	anbi2i	$$⊢\left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)\leftrightarrow \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)$$
10	1 9	bitri	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)$$