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

Metamath Proof Explorer

Theorem feq23i

Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Hypotheses feq23i.1 ⊢ A = C
feq23i.2 ⊢ B = D
Assertion feq23i ⊢ F : A ⟶ B ↔ F : C ⟶ D

Proof

Step Hyp Ref Expression
1 feq23i.1 ⊢ A = C
2 feq23i.2 ⊢ B = D
3 feq23 ⊢ A = C ∧ B = D → F : A ⟶ B ↔ F : C ⟶ D
4 1 2 3 mp2an ⊢ F : A ⟶ B ↔ F : C ⟶ D