Theorem f1veqaeq

Description: If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017)

	Ref	Expression
Assertion	f1veqaeq	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\in A\wedge D\in A\right)\right)\to \left(F\left(C\right)=F\left(D\right)\to C=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		dff13	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall c\in A\forall d\in A\left(F\left(c\right)=F\left(d\right)\to c=d\right)\right)$$
2		fveqeq2	$$⊢c=C\to \left(F\left(c\right)=F\left(d\right)\leftrightarrow F\left(C\right)=F\left(d\right)\right)$$
3		eqeq1	$$⊢c=C\to \left(c=d\leftrightarrow C=d\right)$$
4	2 3	imbi12d	$$⊢c=C\to \left(\left(F\left(c\right)=F\left(d\right)\to c=d\right)\leftrightarrow \left(F\left(C\right)=F\left(d\right)\to C=d\right)\right)$$
5		fveq2	$$⊢d=D\to F\left(d\right)=F\left(D\right)$$
6	5	eqeq2d	$$⊢d=D\to \left(F\left(C\right)=F\left(d\right)\leftrightarrow F\left(C\right)=F\left(D\right)\right)$$
7		eqeq2	$$⊢d=D\to \left(C=d\leftrightarrow C=D\right)$$
8	6 7	imbi12d	$$⊢d=D\to \left(\left(F\left(C\right)=F\left(d\right)\to C=d\right)\leftrightarrow \left(F\left(C\right)=F\left(D\right)\to C=D\right)\right)$$
9	4 8	rspc2v	$$⊢\left(C\in A\wedge D\in A\right)\to \left(\forall c\in A\forall d\in A\left(F\left(c\right)=F\left(d\right)\to c=d\right)\to \left(F\left(C\right)=F\left(D\right)\to C=D\right)\right)$$
10	9	com12	$$⊢\forall c\in A\forall d\in A\left(F\left(c\right)=F\left(d\right)\to c=d\right)\to \left(\left(C\in A\wedge D\in A\right)\to \left(F\left(C\right)=F\left(D\right)\to C=D\right)\right)$$
11	1 10	simplbiim	$$⊢F:A\underset{1-1}{⟶}B\to \left(\left(C\in A\wedge D\in A\right)\to \left(F\left(C\right)=F\left(D\right)\to C=D\right)\right)$$
12	11	imp	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(C\in A\wedge D\in A\right)\right)\to \left(F\left(C\right)=F\left(D\right)\to C=D\right)$$