Metamath Proof Explorer


Syntax definition c3

Description: Extend class notation to include the number 3.

Ref Expression
Assertion c3
class 3