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