Metamath Proof Explorer

Theorem sucdifsn

Description: The difference between the successor and the singleton of a class is the class. (Contributed by Peter Mazsa, 20-Sep-2024)

Ref Expression
Assertion sucdifsn 
|- ( suc A \ { A } ) = A

Proof

Step Hyp Ref Expression
1 df-suc 
 |-  suc A = ( A u. { A } )
2 1 difeq1i 
 |-  ( suc A \ { A } ) = ( ( A u. { A } ) \ { A } )
3 sucdifsn2 
 |-  ( ( A u. { A } ) \ { A } ) = A
4 2 3 eqtri 
 |-  ( suc A \ { A } ) = A