Metamath Proof Explorer

Theorem feq1d

Description: Equality deduction for functions. (Contributed by NM, 19-Feb-2008)

Ref Expression
Hypothesis feq1d.1 
|- ( ph -> F = G )
Assertion feq1d 
|- ( ph -> ( F : A --> B <-> G : A --> B ) )

Proof

Step Hyp Ref Expression
1 feq1d.1 
 |-  ( ph -> F = G )
2 feq1 
 |-  ( F = G -> ( F : A --> B <-> G : A --> B ) )
3 1 2 syl 
 |-  ( ph -> ( F : A --> B <-> G : A --> B ) )