Metamath Proof Explorer


Syntax definition csetrecs

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

Ref Expression
Assertion csetrecs class setrecs ( 𝐹 )