Theorem eldisjss

Description: Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	eldisjss	|- ( A C_ B -> ( ElDisj B -> ElDisj A ) )

Proof

Step	Hyp	Ref	Expression
1		ssres2	|- ( A C_ B -> ( `' _E |` A ) C_ ( `' _E |` B ) )
2	1	disjssd	|- ( A C_ B -> ( Disj ( `' _E |` B ) -> Disj ( `' _E |` A ) ) )
3		df-eldisj	|- ( ElDisj B <-> Disj ( `' _E |` B ) )
4		df-eldisj	|- ( ElDisj A <-> Disj ( `' _E |` A ) )
5	2 3 4	3imtr4g	|- ( A C_ B -> ( ElDisj B -> ElDisj A ) )