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 ⁡ A ∖ A = A

Proof

Step Hyp Ref Expression
1 df-suc ⊢ suc ⁡ A = A ∪ A
2 1 difeq1i ⊢ suc ⁡ A ∖ A = A ∪ A ∖ A
3 sucdifsn2 ⊢ A ∪ A ∖ A = A
4 2 3 eqtri ⊢ suc ⁡ A ∖ A = A