Metamath Proof Explorer

Theorem dfsuccl3

Description: Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 30-Jan-2026)

Ref Expression
Assertion dfsuccl3 
|- Suc = { n | E! m suc m = n }

Proof

Step Hyp Ref Expression
1 dfsuccl2 
 |-  Suc = { n | E. m suc m = n }
2 exeupre2 
 |-  ( E. m suc m = n <-> E! m suc m = n )
3 2 abbii 
 |-  { n | E. m suc m = n } = { n | E! m suc m = n }
4 1 3 eqtri 
 |-  Suc = { n | E! m suc m = n }