indifundif

Description: A remarkable equation with sets. (Contributed by Thierry Arnoux, 18-May-2020)

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

Step	Hyp	Ref	Expression
1		difindi	$⊢ A ∖ (B \cap C) = (A ∖ B) \cup (A ∖ C)$
2		difundir	$⊢ ((A \cap B) \cup (A ∖ B)) ∖ C = ((A \cap B) ∖ C) \cup ((A ∖ B) ∖ C)$
3		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
4	3	difeq1i	$⊢ ((A \cap B) \cup (A ∖ B)) ∖ C = A ∖ C$
5		uncom	$⊢ ((A \cap B) ∖ C) \cup ((A ∖ B) ∖ C) = ((A ∖ B) ∖ C) \cup ((A \cap B) ∖ C)$
6	2 4 5	3eqtr3i	$⊢ A ∖ C = ((A ∖ B) ∖ C) \cup ((A \cap B) ∖ C)$
7	6	uneq2i	$⊢ (A ∖ B) \cup (A ∖ C) = (A ∖ B) \cup (((A ∖ B) ∖ C) \cup ((A \cap B) ∖ C))$
8		unass	$⊢ ((A ∖ B) \cup ((A ∖ B) ∖ C)) \cup ((A \cap B) ∖ C) = (A ∖ B) \cup (((A ∖ B) ∖ C) \cup ((A \cap B) ∖ C))$
9		undifabs	$⊢ (A ∖ B) \cup ((A ∖ B) ∖ C) = A ∖ B$
10	9	uneq1i	$⊢ ((A ∖ B) \cup ((A ∖ B) ∖ C)) \cup ((A \cap B) ∖ C) = (A ∖ B) \cup ((A \cap B) ∖ C)$
11	7 8 10	3eqtr2i	$⊢ (A ∖ B) \cup (A ∖ C) = (A ∖ B) \cup ((A \cap B) ∖ C)$
12		uncom	$⊢ (A ∖ B) \cup ((A \cap B) ∖ C) = ((A \cap B) ∖ C) \cup (A ∖ B)$
13	1 11 12	3eqtrri	$⊢ ((A \cap B) ∖ C) \cup (A ∖ B) = A ∖ (B \cap C)$

Metamath Proof Explorer