Syntax Definition cfrec 6448

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

Hypotheses

Ref	Expression
cF	class F
cI	class I

Assertion

Ref	Expression
cfrec	class frec ( F , I )

See definition df-frec 6449 for more information.