Metamath Proof Explorer


Syntax definition cop

Description: Extend class notation to include ordered pair.

Ref Expression
Assertion cop class A B