Syntax Definition cfrec 6369

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

Hypotheses

Ref	Expression
cF	class 𝐹
cI	class 𝐼

Assertion

Ref	Expression
cfrec	class frec(𝐹, 𝐼)

See definition df-frec 6370 for more information.