Syntax Definition cmpt 5651

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

Hypotheses

Ref	Expression
vx	setvar x
cA	class A
cB	class B

Assertion

Ref	Expression
cmpt	class (x ∈ A ↦ B)

See definition df-mpt 5652 for more information.