Metamath Proof Explorer


Theorem feq12d

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

Ref Expression
Hypotheses feq12d.1
|- ( ph -> F = G )
feq12d.2
|- ( ph -> A = B )
Assertion feq12d
|- ( ph -> ( F : A --> C <-> G : B --> C ) )

Proof

Step Hyp Ref Expression
1 feq12d.1
 |-  ( ph -> F = G )
2 feq12d.2
 |-  ( ph -> A = B )
3 1 feq1d
 |-  ( ph -> ( F : A --> C <-> G : A --> C ) )
4 2 feq2d
 |-  ( ph -> ( G : A --> C <-> G : B --> C ) )
5 3 4 bitrd
 |-  ( ph -> ( F : A --> C <-> G : B --> C ) )