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

Metamath Proof Explorer

Theorem inindif

Description: The intersection and class difference of a class with another class are disjoint. With inundif , this shows that such intersection and class difference partition the class A . (Contributed by Thierry Arnoux, 13-Sep-2017)

		Ref	Expression
	Assertion	inindif	$⊢ (A \cap C) \cap (A ∖ C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		inss2	$⊢ A \cap C \subseteq C$
2		ssinss1	$⊢ A \cap C \subseteq C \to (A \cap C) \cap A \subseteq C$
3	1 2	ax-mp	$⊢ (A \cap C) \cap A \subseteq C$
4		inssdif0	$⊢ (A \cap C) \cap A \subseteq C \leftrightarrow (A \cap C) \cap (A ∖ C) = \emptyset$
5	3 4	mpbi	$⊢ (A \cap C) \cap (A ∖ C) = \emptyset$