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

Metamath Proof Explorer

Theorem feq23d

Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 feq23d.1 ⊢ φ → A = C
2 feq23d.2 ⊢ φ → B = D
3 eqidd ⊢ φ → F = F
4 3 1 2 feq123d ⊢ φ → F : A ⟶ B ↔ F : C ⟶ D