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

Metamath Proof Explorer

Theorem dif32

Description: Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004)

		Ref	Expression
	Assertion	dif32	$⊢ (A ∖ B) ∖ C = (A ∖ C) ∖ B$

Step	Hyp	Ref	Expression
1		uncom	$⊢ B \cup C = C \cup B$
2	1	difeq2i	$⊢ A ∖ (B \cup C) = A ∖ (C \cup B)$
3		difun1	$⊢ A ∖ (B \cup C) = (A ∖ B) ∖ C$
4		difun1	$⊢ A ∖ (C \cup B) = (A ∖ C) ∖ B$
5	2 3 4	3eqtr3i	$⊢ (A ∖ B) ∖ C = (A ∖ C) ∖ B$