difun1

Description: A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004)

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

Step	Hyp	Ref	Expression
1		inass	$⊢ (A \cap (V ∖ B)) \cap (V ∖ C) = A \cap ((V ∖ B) \cap (V ∖ C))$
2		invdif	$⊢ (A \cap (V ∖ B)) \cap (V ∖ C) = (A \cap (V ∖ B)) ∖ C$
3	1 2	eqtr3i	$⊢ A \cap ((V ∖ B) \cap (V ∖ C)) = (A \cap (V ∖ B)) ∖ C$
4		undm	$⊢ V ∖ (B \cup C) = (V ∖ B) \cap (V ∖ C)$
5	4	ineq2i	$⊢ A \cap (V ∖ (B \cup C)) = A \cap ((V ∖ B) \cap (V ∖ C))$
6		invdif	$⊢ A \cap (V ∖ (B \cup C)) = A ∖ (B \cup C)$
7	5 6	eqtr3i	$⊢ A \cap ((V ∖ B) \cap (V ∖ C)) = A ∖ (B \cup C)$
8	3 7	eqtr3i	$⊢ (A \cap (V ∖ B)) ∖ C = A ∖ (B \cup C)$
9		invdif	$⊢ A \cap (V ∖ B) = A ∖ B$
10	9	difeq1i	$⊢ (A \cap (V ∖ B)) ∖ C = (A ∖ B) ∖ C$
11	8 10	eqtr3i	$⊢ A ∖ (B \cup C) = (A ∖ B) ∖ C$

Metamath Proof Explorer