Syntax Definition csuc 2201

Description: Extend class notation to include the successor function.

Hypothesis

Ref	Expression
cA	class A

Assertion

Ref	Expression
csuc	class suc A

See definition df-suc 2205 for more information.

metamath.org