Syntax Definition cmpt 4043

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

Hypotheses

Ref	Expression
vx	setvar 𝑥
cA	class 𝐴
cB	class 𝐵

Assertion

Ref	Expression
cmpt	class (𝑥 ∈ 𝐴 ↦ 𝐵)

See definition df-mpt 4045 for more information.