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	$$⊢\phi \to A\subseteq B$$
	ssdisjdr.2	$$⊢\phi \to C\cap B=\varnothing$$
Assertion	ssdisjdr	$$⊢\phi \to C\cap A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ssdisjd.1	$$⊢\phi \to A\subseteq B$$
2		ssdisjdr.2	$$⊢\phi \to C\cap B=\varnothing$$
3		sslin	$$⊢A\subseteq B\to C\cap A\subseteq C\cap B$$
4	1 3	syl	$$⊢\phi \to C\cap A\subseteq C\cap B$$
5		sseq0	$$⊢\left(C\cap A\subseteq C\cap B\wedge C\cap B=\varnothing \right)\to C\cap A=\varnothing$$
6	4 2 5	syl2anc	$$⊢\phi \to C\cap A=\varnothing$$