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

Metamath Proof Explorer

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 ⊢ A ∖ ∅ = A

Proof

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