This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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