This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1eq2

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

Ref Expression
Assertion f1eq2 ⊢ A = B → F : A ⟶ 1-1 C ↔ F : B ⟶ 1-1 C

Proof

Step Hyp Ref Expression
1 feq2 ⊢ A = B → F : A ⟶ C ↔ F : B ⟶ C
2 1 anbi1d ⊢ A = B → F : A ⟶ C ∧ Fun ⁡ F -1 ↔ F : B ⟶ C ∧ Fun ⁡ F -1
3 df-f1 ⊢ F : A ⟶ 1-1 C ↔ F : A ⟶ C ∧ Fun ⁡ F -1
4 df-f1 ⊢ F : B ⟶ 1-1 C ↔ F : B ⟶ C ∧ Fun ⁡ F -1
5 2 3 4 3bitr4g ⊢ A = B → F : A ⟶ 1-1 C ↔ F : B ⟶ 1-1 C