Syntax Definition crdg 6427

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

Hypotheses

Ref	Expression
cF	class 𝐹
cI	class 𝐼

Assertion

Ref	Expression
crdg	class rec(𝐹, 𝐼)

See definition df-irdg 6428 for more information.