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