This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	\|- ( -. A e. _V <-> suc A = A )

Proof

Step	Hyp	Ref	Expression
1		sucprc	\|- ( -. A e. _V -> suc A = A )
2		elirr	\|- -. A e. A
3		snssg	\|- ( A e. _V -> ( A e. A <-> { A } C_ A ) )
4	2 3	mtbii	\|- ( A e. _V -> -. { A } C_ A )
5		df-suc	\|- suc A = ( A u. { A } )
6	5	eqeq1i	\|- ( suc A = A <-> ( A u. { A } ) = A )
7		ssequn2	\|- ( { A } C_ A <-> ( A u. { A } ) = A )
8	6 7	sylbb2	\|- ( suc A = A -> { A } C_ A )
9	4 8	nsyl3	\|- ( suc A = A -> -. A e. _V )
10	1 9	impbii	\|- ( -. A e. _V <-> suc A = A )