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

Metamath Proof Explorer

Theorem difdif2

Description: Class difference by a class difference. (Contributed by Thierry Arnoux, 18-Dec-2017)

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

Step	Hyp	Ref	Expression
1		difindi	$⊢ A ∖ (B \cap (V ∖ C)) = (A ∖ B) \cup (A ∖ (V ∖ C))$
2		invdif	$⊢ B \cap (V ∖ C) = B ∖ C$
3	2	eqcomi	$⊢ B ∖ C = B \cap (V ∖ C)$
4	3	difeq2i	$⊢ A ∖ (B ∖ C) = A ∖ (B \cap (V ∖ C))$
5		dfin2	$⊢ A \cap C = A ∖ (V ∖ C)$
6	5	uneq2i	$⊢ (A ∖ B) \cup (A \cap C) = (A ∖ B) \cup (A ∖ (V ∖ C))$
7	1 4 6	3eqtr4i	$⊢ A ∖ (B ∖ C) = (A ∖ B) \cup (A \cap C)$