Syntax Definition cmpo 5776

Description: Extend the definition of a class to include maps-to notation for defining an operation via a rule.

Hypotheses

Ref	Expression
vx	setvar 𝑥
vy	setvar 𝑦
cA	class 𝐴
cB	class 𝐵
cC	class 𝐶

Assertion

Ref	Expression
cmpo	class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)

See definition df-mpo 5779 for more information.