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	⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		difun1	⊢ ( 𝐴 ∖ ( 𝐵 ∪ 𝐵 ) ) = ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐵 )
2		unidm	⊢ ( 𝐵 ∪ 𝐵 ) = 𝐵
3	2	difeq2i	⊢ ( 𝐴 ∖ ( 𝐵 ∪ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
4	1 3	eqtr3i	⊢ ( ( 𝐴 ∖ 𝐵 ) ∖ 𝐵 ) = ( 𝐴 ∖ 𝐵 )