Metamath Proof Explorer

Theorem f1oeq1

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

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

Proof

Step Hyp Ref Expression
1 f1eq1 
 |-  ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )
2 foeq1 
 |-  ( F = G -> ( F : A -onto-> B <-> G : A -onto-> B ) )
3 1 2 anbi12d 
 |-  ( F = G -> ( ( F : A -1-1-> B /\ F : A -onto-> B ) <-> ( G : A -1-1-> B /\ G : A -onto-> B ) ) )
4 df-f1o 
 |-  ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
5 df-f1o 
 |-  ( G : A -1-1-onto-> B <-> ( G : A -1-1-> B /\ G : A -onto-> B ) )
6 3 4 5 3bitr4g 
 |-  ( F = G -> ( F : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )