Metamath Proof Explorer


Syntax definition cop

Description: Extend class notation to include ordered pair.

Ref Expression
Assertion cop
class <. A , B >.