crdg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > crdg		Structured version Visualization version GIF version

Syntax Definition crdg 8240

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-rdg 8241 for more information.

Colors of variables: wff setvar class