Theorem ssdisjdr

Description: Subset preserves disjointness. Deduction form of ssdisj . Alternatively this could be proved with ineqcom in tandem with ssdisjd . (Contributed by Zhi Wang, 7-Sep-2024)

	Ref	Expression
Hypotheses	ssdisjd.1	|- ( ph -> A C_ B )
	ssdisjdr.2	|- ( ph -> ( C i^i B ) = (/) )
Assertion	ssdisjdr	|- ( ph -> ( C i^i A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		ssdisjd.1	|- ( ph -> A C_ B )
2		ssdisjdr.2	|- ( ph -> ( C i^i B ) = (/) )
3		sslin	|- ( A C_ B -> ( C i^i A ) C_ ( C i^i B ) )
4	1 3	syl	|- ( ph -> ( C i^i A ) C_ ( C i^i B ) )
5		sseq0	|- ( ( ( C i^i A ) C_ ( C i^i B ) /\ ( C i^i B ) = (/) ) -> ( C i^i A ) = (/) )
6	4 2 5	syl2anc	|- ( ph -> ( C i^i A ) = (/) )