Theorem ssdisjd

Description: Subset preserves disjointness. Deduction form of ssdisj . (Contributed by Zhi Wang, 7-Sep-2024)

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

Proof

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