Metamath Proof Explorer


Theorem funALTVeqd

Description: Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013)

Ref Expression
Hypothesis funALTVeqd.1
|- ( ph -> A = B )
Assertion funALTVeqd
|- ( ph -> ( FunALTV A <-> FunALTV B ) )

Proof

Step Hyp Ref Expression
1 funALTVeqd.1
 |-  ( ph -> A = B )
2 funALTVeq
 |-  ( A = B -> ( FunALTV A <-> FunALTV B ) )
3 1 2 syl
 |-  ( ph -> ( FunALTV A <-> FunALTV B ) )