Metamath Proof Explorer

Theorem feq12d

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

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

Proof

Step Hyp Ref Expression
1 feq12d.1 ⊢ φ → F = G
2 feq12d.2 ⊢ φ → A = B
3 1 feq1d ⊢ φ → F : A ⟶ C ↔ G : A ⟶ C
4 2 feq2d ⊢ φ → G : A ⟶ C ↔ G : B ⟶ C
5 3 4 bitrd ⊢ φ → F : A ⟶ C ↔ G : B ⟶ C