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)

	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		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
4	3	eqeq1i	$$⊢\mathrm{suc}A=A\leftrightarrow A\cup \left\{A\right\}=A$$
5		ssequn2	$$⊢\left\{A\right\}\subseteq A\leftrightarrow A\cup \left\{A\right\}=A$$
6	4 5	sylbb2	$$⊢\mathrm{suc}A=A\to \left\{A\right\}\subseteq A$$
7		snidg	$$⊢A\in \mathrm{V}\to A\in \left\{A\right\}$$
8		ssel2	$$⊢\left(\left\{A\right\}\subseteq A\wedge A\in \left\{A\right\}\right)\to A\in A$$
9	6 7 8	syl2an	$$⊢\left(\mathrm{suc}A=A\wedge A\in \mathrm{V}\right)\to A\in A$$
10	2 9	mto	$$⊢\neg \left(\mathrm{suc}A=A\wedge A\in \mathrm{V}\right)$$
11	10	imnani	$$⊢\mathrm{suc}A=A\to \neg A\in \mathrm{V}$$
12	1 11	impbii	$$⊢\neg A\in \mathrm{V}\leftrightarrow \mathrm{suc}A=A$$