Metamath Proof Explorer


Theorem funALTVeq

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

Ref Expression
Assertion funALTVeq A=BFunALTVAFunALTVB

Proof

Step Hyp Ref Expression
1 eqimss2 A=BBA
2 funALTVss BAFunALTVAFunALTVB
3 1 2 syl A=BFunALTVAFunALTVB
4 eqimss A=BAB
5 funALTVss ABFunALTVBFunALTVA
6 4 5 syl A=BFunALTVBFunALTVA
7 3 6 impbid A=BFunALTVAFunALTVB