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

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 𝐴 ∖ { 𝐴 } ) = 𝐴

Proof

Step Hyp Ref Expression
1 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
2 1 difeq1i ⊢ ( suc 𝐴 ∖ { 𝐴 } ) = ( ( 𝐴 ∪ { 𝐴 } ) ∖ { 𝐴 } )
3 sucdifsn2 ⊢ ( ( 𝐴 ∪ { 𝐴 } ) ∖ { 𝐴 } ) = 𝐴
4 2 3 eqtri ⊢ ( suc 𝐴 ∖ { 𝐴 } ) = 𝐴