cm - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition cm 4340

Description: Extend the definition of a class to include the mapping operation. (Read for A ↑_m B, "the set of all functions that map from B to A.)

**Assertion**
Ref	Expression
cm	class ↑_m

See definition df-map 4342 for more information.

Colors of variables: wff set class