Metamath Proof Explorer


Syntax definition cgdlop2

Description: Extend the definition of a class to include the second Gödel operation.

Ref Expression
Assertion cgdlop2 class ℱ2