Metamath Proof Explorer

Theorem feq1i

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

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

Proof

Step Hyp Ref Expression
1 feq1i.1 
 |-  F = G
2 feq1 
 |-  ( F = G -> ( F : A --> B <-> G : A --> B ) )
3 1 2 ax-mp 
 |-  ( F : A --> B <-> G : A --> B )