inindif

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

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

Metamath Proof Explorer