Metamath Proof Explorer


Theorem funALTVeqd

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

Ref Expression
Hypothesis funALTVeqd.1 ( 𝜑𝐴 = 𝐵 )
Assertion funALTVeqd ( 𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵 ) )

Proof

Step Hyp Ref Expression
1 funALTVeqd.1 ( 𝜑𝐴 = 𝐵 )
2 funALTVeq ( 𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵 ) )
3 1 2 syl ( 𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵 ) )