Syntax Definition cmpo 7257

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 7260 for more information.