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