Metamath Proof Explorer


Theorem funALTVss

Description: Subclass theorem for function. (Contributed by NM, 16-Aug-1994) (Proof shortened by Mario Carneiro, 24-Jun-2014) (Revised by Peter Mazsa, 22-Sep-2021)

Ref Expression
Assertion funALTVss A B FunALTV B FunALTV A

Proof

Step Hyp Ref Expression
1 cossss A B A B
2 sstr2 A B B I A I
3 1 2 syl A B B I A I
4 relss A B Rel B Rel A
5 3 4 anim12d A B B I Rel B A I Rel A
6 dffunALTV2 FunALTV B B I Rel B
7 dffunALTV2 FunALTV A A I Rel A
8 5 6 7 3imtr4g A B FunALTV B FunALTV A