Metamath Proof Explorer


Syntax definition csuc

Description: Extend class notation to include the successor function.

Ref Expression
Assertion csuc class suc 𝐴