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

Metamath Proof Explorer

Theorem difindir

Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004)

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

Step	Hyp	Ref	Expression
1		inindir	$⊢ (A \cap B) \cap (V ∖ C) = (A \cap (V ∖ C)) \cap (B \cap (V ∖ C))$
2		invdif	$⊢ (A \cap B) \cap (V ∖ C) = (A \cap B) ∖ C$
3		invdif	$⊢ A \cap (V ∖ C) = A ∖ C$
4		invdif	$⊢ B \cap (V ∖ C) = B ∖ C$
5	3 4	ineq12i	$⊢ (A \cap (V ∖ C)) \cap (B \cap (V ∖ C)) = (A ∖ C) \cap (B ∖ C)$
6	1 2 5	3eqtr3i	$⊢ (A \cap B) ∖ C = (A ∖ C) \cap (B ∖ C)$