csuc - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition csuc 2946

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 2950 for more information.

Colors of variables: wff set class