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

Metamath Proof Explorer

Theorem feq23

Description: Equality theorem for functions. (Contributed by FL, 14-Jul-2007) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion feq23 ⊢ A = C ∧ B = D → F : A ⟶ B ↔ F : C ⟶ D

Proof

Step Hyp Ref Expression
1 feq2 ⊢ A = C → F : A ⟶ B ↔ F : C ⟶ B
2 feq3 ⊢ B = D → F : C ⟶ B ↔ F : C ⟶ D
3 1 2 sylan9bb ⊢ A = C ∧ B = D → F : A ⟶ B ↔ F : C ⟶ D