Metamath Proof Explorer

Theorem dfsuccl2

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

Ref Expression
Assertion dfsuccl2 
|- Suc = { n | E. m suc m = n }

Proof

Step Hyp Ref Expression
1 df-succl 
 |-  Suc = ran SucMap
2 df-sucmap 
 |-  SucMap = { <. m , n >. | suc m = n }
3 2 rneqi 
 |-  ran SucMap = ran { <. m , n >. | suc m = n }
4 rnopab 
 |-  ran { <. m , n >. | suc m = n } = { n | E. m suc m = n }
5 1 3 4 3eqtri 
 |-  Suc = { n | E. m suc m = n }