Metamath Proof Explorer

Theorem f1oeq23

Description: Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012)

Ref Expression
Assertion f1oeq23 ⊢ A = B ∧ C = D → F : A ⟶ 1-1 onto C ↔ F : B ⟶ 1-1 onto D

Proof

Step Hyp Ref Expression
1 f1oeq2 ⊢ A = B → F : A ⟶ 1-1 onto C ↔ F : B ⟶ 1-1 onto C
2 f1oeq3 ⊢ C = D → F : B ⟶ 1-1 onto C ↔ F : B ⟶ 1-1 onto D
3 1 2 sylan9bb ⊢ A = B ∧ C = D → F : A ⟶ 1-1 onto C ↔ F : B ⟶ 1-1 onto D