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 C_ B -> ( FunALTV B -> FunALTV A ) )

Proof

Step Hyp Ref Expression
1 cossss
 |-  ( A C_ B -> ,~ A C_ ,~ B )
2 sstr2
 |-  ( ,~ A C_ ,~ B -> ( ,~ B C_ _I -> ,~ A C_ _I ) )
3 1 2 syl
 |-  ( A C_ B -> ( ,~ B C_ _I -> ,~ A C_ _I ) )
4 relss
 |-  ( A C_ B -> ( Rel B -> Rel A ) )
5 3 4 anim12d
 |-  ( A C_ B -> ( ( ,~ B C_ _I /\ Rel B ) -> ( ,~ A C_ _I /\ Rel A ) ) )
6 dffunALTV2
 |-  ( FunALTV B <-> ( ,~ B C_ _I /\ Rel B ) )
7 dffunALTV2
 |-  ( FunALTV A <-> ( ,~ A C_ _I /\ Rel A ) )
8 5 6 7 3imtr4g
 |-  ( A C_ B -> ( FunALTV B -> FunALTV A ) )