Metamath Proof Explorer


Syntax definition csetrecs

Description: Extend class notation to include a set defined by transfinite recursion.

Ref Expression
Assertion csetrecs
class setrecs ( F )