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

Metamath Proof Explorer

Theorem feq3dd

Description: Equality deduction for functions. (Contributed by Thierry Arnoux, 27-May-2025)

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

Proof

Step Hyp Ref Expression
1 feq3dd.eq ⊢ φ → B = C
2 feq3dd.f ⊢ φ → F : A ⟶ B
3 1 feq3d ⊢ φ → F : A ⟶ B ↔ F : A ⟶ C
4 2 3 mpbid ⊢ φ → F : A ⟶ C