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