Theorem sucprc

Description: A proper class is its own successor. (Contributed by NM, 3-Apr-1995)

	Ref	Expression
Assertion	sucprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{suc}A=A$$

Proof

Step	Hyp	Ref	Expression
1		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
2	1	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
3	2	uneq2d	$$⊢\neg A\in \mathrm{V}\to A\cup \left\{A\right\}=A\cup \varnothing$$
4		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
5		un0	$$⊢A\cup \varnothing =A$$
6	5	eqcomi	$$⊢A=A\cup \varnothing$$
7	3 4 6	3eqtr4g	$$⊢\neg A\in \mathrm{V}\to \mathrm{suc}A=A$$