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	$$⊢\mathrm{suc}A\setminus \left\{A\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
2	1	difeq1i	$$⊢\mathrm{suc}A\setminus \left\{A\right\}=\left(A\cup \left\{A\right\}\right)\setminus \left\{A\right\}$$
3		sucdifsn2	$$⊢\left(A\cup \left\{A\right\}\right)\setminus \left\{A\right\}=A$$
4	2 3	eqtri	$$⊢\mathrm{suc}A\setminus \left\{A\right\}=A$$