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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sucprc | |
|
2 | elirr | |
|
3 | df-suc | |
|
4 | 3 | eqeq1i | |
5 | ssequn2 | |
|
6 | 4 5 | sylbb2 | |
7 | snidg | |
|
8 | ssel2 | |
|
9 | 6 7 8 | syl2an | |
10 | 2 9 | mto | |
11 | 10 | imnani | |
12 | 1 11 | impbii | |