Metamath Proof Explorer

Theorem f1oeq2

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

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

Proof

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