Metamath Proof Explorer


Theorem f1oeq3d

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis f1oeq3d.1
|- ( ph -> A = B )
Assertion f1oeq3d
|- ( ph -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )

Proof

Step Hyp Ref Expression
1 f1oeq3d.1
 |-  ( ph -> A = B )
2 f1oeq3
 |-  ( A = B -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )
3 1 2 syl
 |-  ( ph -> ( F : C -1-1-onto-> A <-> F : C -1-1-onto-> B ) )