Theorem ssdisj

Description: Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007) (Proof shortened by JJ, 14-Jul-2021)

	Ref	Expression
Assertion	ssdisj	$$⊢\left(A\subseteq B\wedge B\cap C=\varnothing \right)\to A\cap C=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ssrin	$$⊢A\subseteq B\to A\cap C\subseteq B\cap C$$
2		eqimss	$$⊢B\cap C=\varnothing \to B\cap C\subseteq \varnothing$$
3	1 2	sylan9ss	$$⊢\left(A\subseteq B\wedge B\cap C=\varnothing \right)\to A\cap C\subseteq \varnothing$$
4		ss0	$$⊢A\cap C\subseteq \varnothing \to A\cap C=\varnothing$$
5	3 4	syl	$$⊢\left(A\subseteq B\wedge B\cap C=\varnothing \right)\to A\cap C=\varnothing$$