Metamath Proof Explorer


Syntax definition cwsuc

Description: Declare the syntax for well-founded successor.

Ref Expression
Assertion cwsuc
class wsuc ( R , A , X )