ssin0

Description: If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	ssin0	$⊢ (A \cap B = \emptyset \land C \subseteq A \land D \subseteq B) \to C \cap D = \emptyset$

Step	Hyp	Ref	Expression
1		ss2in	$⊢ (C \subseteq A \land D \subseteq B) \to C \cap D \subseteq A \cap B$
2	1	3adant1	$⊢ (A \cap B = \emptyset \land C \subseteq A \land D \subseteq B) \to C \cap D \subseteq A \cap B$
3		eqimss	$⊢ A \cap B = \emptyset \to A \cap B \subseteq \emptyset$
4	3	3ad2ant1	$⊢ (A \cap B = \emptyset \land C \subseteq A \land D \subseteq B) \to A \cap B \subseteq \emptyset$
5	2 4	sstrd	$⊢ (A \cap B = \emptyset \land C \subseteq A \land D \subseteq B) \to C \cap D \subseteq \emptyset$
6		ss0	$⊢ C \cap D \subseteq \emptyset \to C \cap D = \emptyset$
7	5 6	syl	$⊢ (A \cap B = \emptyset \land C \subseteq A \land D \subseteq B) \to C \cap D = \emptyset$

Metamath Proof Explorer