Theorem disjss

Description: Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020) (Revised by Peter Mazsa, 22-Sep-2021)

	Ref	Expression
Assertion	disjss	|- ( A C_ B -> ( Disj B -> Disj A ) )

Proof

Step	Hyp	Ref	Expression
1		cnvss	|- ( A C_ B -> `' A C_ `' B )
2		funALTVss	|- ( `' A C_ `' B -> ( FunALTV `' B -> FunALTV `' A ) )
3	1 2	syl	|- ( A C_ B -> ( FunALTV `' B -> FunALTV `' A ) )
4		relss	|- ( A C_ B -> ( Rel B -> Rel A ) )
5	3 4	anim12d	|- ( A C_ B -> ( ( FunALTV `' B /\ Rel B ) -> ( FunALTV `' A /\ Rel A ) ) )
6		dfdisjALTV	|- ( Disj B <-> ( FunALTV `' B /\ Rel B ) )
7		dfdisjALTV	|- ( Disj A <-> ( FunALTV `' A /\ Rel A ) )
8	5 6 7	3imtr4g	|- ( A C_ B -> ( Disj B -> Disj A ) )