Metamath Proof Explorer


Theorem funALTVeq

Description: Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994)

Ref Expression
Assertion funALTVeq A = B FunALTV A FunALTV B

Proof

Step Hyp Ref Expression
1 eqimss2 A = B B A
2 funALTVss B A FunALTV A FunALTV B
3 1 2 syl A = B FunALTV A FunALTV B
4 eqimss A = B A B
5 funALTVss A B FunALTV B FunALTV A
6 4 5 syl A = B FunALTV B FunALTV A
7 3 6 impbid A = B FunALTV A FunALTV B