Syntax Definition crdg 2969

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

metamath.org