Metamath Proof Explorer

Theorem f1resveqaeq

Description: If a function restricted to a class is one-to-one, then for any two elements of the class, the values of the function at those elements are equal only if the two elements are the same element. (Contributed by BTernaryTau, 27-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 fvres 
 |-  ( C e. A -> ( ( F |` A ) ` C ) = ( F ` C ) )
2 1 ad2antrl 
 |-  ( ( ( F |` A ) : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F |` A ) ` C ) = ( F ` C ) )
3 fvres 
 |-  ( D e. A -> ( ( F |` A ) ` D ) = ( F ` D ) )
4 3 ad2antll 
 |-  ( ( ( F |` A ) : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F |` A ) ` D ) = ( F ` D ) )
5 2 4 eqeq12d 
 |-  ( ( ( F |` A ) : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( ( F |` A ) ` C ) = ( ( F |` A ) ` D ) <-> ( F ` C ) = ( F ` D ) ) )
6 f1veqaeq 
 |-  ( ( ( F |` A ) : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( ( F |` A ) ` C ) = ( ( F |` A ) ` D ) -> C = D ) )
7 5 6 sylbird 
 |-  ( ( ( F |` A ) : A -1-1-> B /\ ( C e. A /\ D e. A ) ) -> ( ( F ` C ) = ( F ` D ) -> C = D ) )