Syntax Definition co 3001

Description: Extend class notation to include operations. Note that the syntax is simply three class symbols in a row surrounded by parentheses.

Hypotheses

Ref	Expression
cA	class A
cB	class B
cF	class F

Assertion

Ref	Expression
co	class (AFB)

See definition df-opr 3003 for more information.

metamath.org