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	|- ( -. 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		df-suc	|- suc A = ( A u. { A } )
4	3	eqeq1i	|- ( suc A = A <-> ( A u. { A } ) = A )
5		ssequn2	|- ( { A } C_ A <-> ( A u. { A } ) = A )
6	4 5	sylbb2	|- ( suc A = A -> { A } C_ A )
7		snidg	|- ( A e. _V -> A e. { A } )
8		ssel2	|- ( ( { A } C_ A /\ A e. { A } ) -> A e. A )
9	6 7 8	syl2an	|- ( ( suc A = A /\ A e. _V ) -> A e. A )
10	2 9	mto	|- -. ( suc A = A /\ A e. _V )
11	10	imnani	|- ( suc A = A -> -. A e. _V )
12	1 11	impbii	|- ( -. A e. _V <-> suc A = A )