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