Metamath Proof Explorer


Syntax definition cr1

Description: Extend class definition to include the cumulative hierarchy of sets function.

Ref Expression
Assertion cr1 class R1