Theorem sucprcreg

Description: A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004) (Proof shortened by BJ, 16-Apr-2019) (Proof shortened by SN, 22-Apr-2026)

	Ref	Expression
Assertion	sucprcreg	$$⊢\neg A\in \mathrm{V}\leftrightarrow \mathrm{suc}A=A$$

Proof

Step	Hyp	Ref	Expression
1		sucprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{suc}A=A$$
2		elirr	$$⊢\neg A\in A$$
3		snssg	$$⊢A\in \mathrm{V}\to \left(A\in A\leftrightarrow \left\{A\right\}\subseteq A\right)$$
4	2 3	mtbii	$$⊢A\in \mathrm{V}\to \neg \left\{A\right\}\subseteq A$$
5		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
6	5	eqeq1i	$$⊢\mathrm{suc}A=A\leftrightarrow A\cup \left\{A\right\}=A$$
7		ssequn2	$$⊢\left\{A\right\}\subseteq A\leftrightarrow A\cup \left\{A\right\}=A$$
8	6 7	sylbb2	$$⊢\mathrm{suc}A=A\to \left\{A\right\}\subseteq A$$
9	4 8	nsyl3	$$⊢\mathrm{suc}A=A\to \neg A\in \mathrm{V}$$
10	1 9	impbii	$$⊢\neg A\in \mathrm{V}\leftrightarrow \mathrm{suc}A=A$$