Metamath Proof Explorer


Syntax definition cphi

Description: Extend class notation with the Euler phi function.

Ref Expression
Assertion cphi
class phi