Metamath Proof Explorer


Syntax definition cpc

Description: Extend class notation with the prime count function.

Ref Expression
Assertion cpc class pCnt