Metamath Proof Explorer

Theorem f1eq1

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997)

Ref Expression
Assertion f1eq1 
|- ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )

Proof

Step Hyp Ref Expression
1 feq1 
 |-  ( F = G -> ( F : A --> B <-> G : A --> B ) )
2 cnveq 
 |-  ( F = G -> `' F = `' G )
3 2 funeqd 
 |-  ( F = G -> ( Fun `' F <-> Fun `' G ) )
4 1 3 anbi12d 
 |-  ( F = G -> ( ( F : A --> B /\ Fun `' F ) <-> ( G : A --> B /\ Fun `' G ) ) )
5 df-f1 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
6 df-f1 
 |-  ( G : A -1-1-> B <-> ( G : A --> B /\ Fun `' G ) )
7 4 5 6 3bitr4g 
 |-  ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )