Metamath Proof Explorer

Theorem f1oeq3

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

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

Proof

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