Metamath Proof Explorer


Syntax definition crdg

Description: Extend class notation with the recursive definition generator, with characteristic function F and initial value I .

Ref Expression
Assertion crdg
class rec ( F , I )