Theorem dif0

Description: The difference between a class and the empty set. Part of Exercise 4.4 of Stoll p. 16. (Contributed by NM, 17-Aug-2004)

	Ref	Expression
Assertion	dif0	⊢ ( 𝐴 ∖ ∅ ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		difid	⊢ ( 𝐴 ∖ 𝐴 ) = ∅
2	1	difeq2i	⊢ ( 𝐴 ∖ ( 𝐴 ∖ 𝐴 ) ) = ( 𝐴 ∖ ∅ )
3		difdif	⊢ ( 𝐴 ∖ ( 𝐴 ∖ 𝐴 ) ) = 𝐴
4	2 3	eqtr3i	⊢ ( 𝐴 ∖ ∅ ) = 𝐴