Metamath Proof Explorer


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 ) )