difundi

Description: Distributive law for class difference. Theorem 39 of Suppes p. 29. (Contributed by NM, 17-Aug-2004)

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

Step	Hyp	Ref	Expression
1		dfun3	$⊢ B \cup C = V ∖ ((V ∖ B) \cap (V ∖ C))$
2	1	difeq2i	$⊢ A ∖ (B \cup C) = A ∖ (V ∖ ((V ∖ B) \cap (V ∖ C)))$
3		inindi	$⊢ A \cap ((V ∖ B) \cap (V ∖ C)) = (A \cap (V ∖ B)) \cap (A \cap (V ∖ C))$
4		dfin2	$⊢ A \cap ((V ∖ B) \cap (V ∖ C)) = A ∖ (V ∖ ((V ∖ B) \cap (V ∖ C)))$
5		invdif	$⊢ A \cap (V ∖ B) = A ∖ B$
6		invdif	$⊢ A \cap (V ∖ C) = A ∖ C$
7	5 6	ineq12i	$⊢ (A \cap (V ∖ B)) \cap (A \cap (V ∖ C)) = (A ∖ B) \cap (A ∖ C)$
8	3 4 7	3eqtr3i	$⊢ A ∖ (V ∖ ((V ∖ B) \cap (V ∖ C))) = (A ∖ B) \cap (A ∖ C)$
9	2 8	eqtri	$⊢ A ∖ (B \cup C) = (A ∖ B) \cap (A ∖ C)$

Metamath Proof Explorer