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

Metamath Proof Explorer

Theorem feq1dd

Description: Equality deduction for functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses feq1dd.eq ⊢ φ → F = G
feq1dd.f ⊢ φ → F : A ⟶ B
Assertion feq1dd ⊢ φ → G : A ⟶ B

Proof

Step Hyp Ref Expression
1 feq1dd.eq ⊢ φ → F = G
2 feq1dd.f ⊢ φ → F : A ⟶ B
3 1 feq1d ⊢ φ → F : A ⟶ B ↔ G : A ⟶ B
4 2 3 mpbid ⊢ φ → G : A ⟶ B