Metamath Proof Explorer


Syntax definition csuc

Description: Extend class notation to include the successor function.

Ref Expression
Assertion csuc
class suc A