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	|- ( ( F : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) )

Proof

Step	Hyp	Ref	Expression
1		dff13	|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. c e. A A. d e. A ( ( F ` c ) = ( F ` d ) -> c = d ) ) )
2		fveqeq2	|- ( c = C -> ( ( F ` c ) = ( F ` d ) <-> ( F ` C ) = ( F ` d ) ) )
3		eqeq1	|- ( c = C -> ( c = d <-> C = d ) )
4	2 3	imbi12d	|- ( c = C -> ( ( ( F ` c ) = ( F ` d ) -> c = d ) <-> ( ( F ` C ) = ( F ` d ) -> C = d ) ) )
5		fveq2	|- ( d = D -> ( F ` d ) = ( F ` D ) )
6	5	eqeq2d	|- ( d = D -> ( ( F ` C ) = ( F ` d ) <-> ( F ` C ) = ( F ` D ) ) )
7		eqeq2	|- ( d = D -> ( C = d <-> C = D ) )
8	6 7	imbi12d	|- ( d = D -> ( ( ( F ` C ) = ( F ` d ) -> C = d ) <-> ( ( F ` C ) = ( F ` D ) -> C = D ) ) )
9	4 8	rspc2v	|- ( ( C e. A /\ D e. A ) -> ( A. c e. A A. d e. A ( ( F ` c ) = ( F ` d ) -> c = d ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) ) )
10	9	com12	|- ( A. c e. A A. d e. A ( ( F ` c ) = ( F ` d ) -> c = d ) -> ( ( C e. A /\ D e. A ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) ) )
11	1 10	simplbiim	|- ( F : A -1-1-> B -> ( ( C e. A /\ D e. A ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) ) )
12	11	imp	|- ( ( F : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) )