Syntax Definition cop 1810

Description: Extend class notation to include ordered pair.

Hypotheses

Ref	Expression
cA	class A
cB	class B

Assertion

Ref	Expression
cop	class ⟨A, B⟩

See definition df-op 1815 for more information.

metamath.org