Metamath Proof Explorer

Theorem feq3d

Description: Equality deduction for functions. (Contributed by AV, 1-Jan-2020)

Ref Expression
Hypothesis feq2d.1 
|- ( ph -> A = B )
Assertion feq3d 
|- ( ph -> ( F : X --> A <-> F : X --> B ) )

Proof

Step Hyp Ref Expression
1 feq2d.1 
 |-  ( ph -> A = B )
2 feq3 
 |-  ( A = B -> ( F : X --> A <-> F : X --> B ) )
3 1 2 syl 
 |-  ( ph -> ( F : X --> A <-> F : X --> B ) )