Metamath Proof Explorer


Syntax definition ceven

Description: Extend the definition of a class to include the set of even numbers.

Ref Expression
Assertion ceven
class Even