crdg - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition crdg 3937

Description: Extend class notation with the recursive definition generator.

**Hypotheses**
Ref	Expression
cA	class A
cB	class B

**Assertion**
Ref	Expression
crdg	class rec(A, B)

See definition df-rdg 3938 for more information.

Colors of variables: wff set class