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

Metamath Proof Explorer

Theorem difabs

Description: Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009)

		Ref	Expression
	Assertion	difabs	$⊢ (A ∖ B) ∖ B = A ∖ B$

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