Metamath Proof Explorer


Syntax definition cgdlop1

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

Ref Expression
Assertion cgdlop1
class ~F1