Metamath Proof Explorer


Syntax definition cxpc

Description: Extend class notation with the product of two categories.

Ref Expression
Assertion cxpc class ×c