Home
Metamath Proof Explorer
< Previous
Next >
Related theorems
Unicode version
Syntax Definition
cm
3258
Description:
Extend the definition of a class to include the mapping operation. (Read for
, "the set of all functions that map from
to
.)
Assertion
Ref
Expression
cm
See definition
df-map
3259
for more information.
Colors of variables:
wff
set
class
metamath.org