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

Metamath Proof Explorer

Theorem f1ocnvfvrneq

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

Ref Expression
Assertion f1ocnvfvrneq 
|- ( ( F : A -1-1-> B /\ ( C e. ran F /\ D e. ran F ) ) -> ( ( `' F ` C ) = ( `' F ` D ) -> C = D ) )

Proof

Step Hyp Ref Expression
1 f1f1orn 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
2 f1ocnv 
 |-  ( F : A -1-1-onto-> ran F -> `' F : ran F -1-1-onto-> A )
3 f1of1 
 |-  ( `' F : ran F -1-1-onto-> A -> `' F : ran F -1-1-> A )
4 f1veqaeq 
 |-  ( ( `' F : ran F -1-1-> A /\ ( C e. ran F /\ D e. ran F ) ) -> ( ( `' F ` C ) = ( `' F ` D ) -> C = D ) )
5 4 ex 
 |-  ( `' F : ran F -1-1-> A -> ( ( C e. ran F /\ D e. ran F ) -> ( ( `' F ` C ) = ( `' F ` D ) -> C = D ) ) )
6 1 2 3 5 4syl 
 |-  ( F : A -1-1-> B -> ( ( C e. ran F /\ D e. ran F ) -> ( ( `' F ` C ) = ( `' F ` D ) -> C = D ) ) )
7 6 imp 
 |-  ( ( F : A -1-1-> B /\ ( C e. ran F /\ D e. ran F ) ) -> ( ( `' F ` C ) = ( `' F ` D ) -> C = D ) )