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 V suc A = A

Proof

Step Hyp Ref Expression
1 sucprc ¬ A V suc A = A
2 elirr ¬ A A
3 df-suc suc A = A A
4 3 eqeq1i suc A = A A A = A
5 ssequn2 A A A A = A
6 4 5 sylbb2 suc A = A A A
7 snidg A V A A
8 ssel2 A A A A A A
9 6 7 8 syl2an suc A = A A V A A
10 2 9 mto ¬ suc A = A A V
11 10 imnani suc A = A ¬ A V
12 1 11 impbii ¬ A V suc A = A