Syntax Definition crdg 6266

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

Hypotheses

Ref	Expression
cF	class F
cI	class I

Assertion

Ref	Expression
crdg	class rec ( F , I )

See definition df-irdg 6267 for more information.