Syntax Definition ctp 3578

Description: Extend class notation to include unordered triplet.

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵
cC	class 𝐶

Assertion

Ref	Expression
ctp	class {𝐴, 𝐵, 𝐶}

See definition df-pr 3583 for more information.