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

Metamath Proof Explorer

Theorem indifdir

Description: Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011) (Revised by BTernaryTau, 14-Aug-2024)

		Ref	Expression
	Assertion	indifdir	$⊢ (A ∖ B) \cap C = (A \cap C) ∖ (B \cap C)$

Step	Hyp	Ref	Expression
1		indifdi	$⊢ C \cap (A ∖ B) = (C \cap A) ∖ (C \cap B)$
2		incom	$⊢ (A ∖ B) \cap C = C \cap (A ∖ B)$
3		incom	$⊢ A \cap C = C \cap A$
4		incom	$⊢ B \cap C = C \cap B$
5	3 4	difeq12i	$⊢ (A \cap C) ∖ (B \cap C) = (C \cap A) ∖ (C \cap B)$
6	1 2 5	3eqtr4i	$⊢ (A ∖ B) \cap C = (A \cap C) ∖ (B \cap C)$