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)

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 )