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 ¬AVsucA=A

Proof

Step Hyp Ref Expression
1 sucprc ¬AVsucA=A
2 elirr ¬AA
3 df-suc sucA=AA
4 3 eqeq1i sucA=AAA=A
5 ssequn2 AAAA=A
6 4 5 sylbb2 sucA=AAA
7 snidg AVAA
8 ssel2 AAAAAA
9 6 7 8 syl2an sucA=AAVAA
10 2 9 mto ¬sucA=AAV
11 10 imnani sucA=A¬AV
12 1 11 impbii ¬AVsucA=A