This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \subseteq B \land B \cap C = \emptyset) \to A \cap C = \emptyset$

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