**Description: **Define the value of a
function, ,
also known as function
application. For example, (we prove this in cos0 12304
after we define cosine in df-cos 12226). Typically function is
defined using maps-to notation (see df-mpt 3976 and df-mpt2 5715), but this
is not required. For example,
(ex-fv 20643).
Note that df-ov 5713 will define two-argument functions using
ordered pairs
as .
Although based on the idea
embodied by Definition 10.2 of [Quine] p.
65 (see args 4948), our
definition apparently does not appear in the literature. However, it is
quite convenient: it can be applied to any class and evaluates to the
empty set when it is not meaningful (as shown by ndmfv 5405 and fvprc 5374).
The left apostrophe notation originated with Peano and was adopted in
Definition *30.01 of [WhiteheadRussell] p. 235, Definition
10.11 of
[Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means
the same thing as the more familiar notation for a
function's value at , i.e. " of ,"
but without
context-dependent notational ambiguity. Alternate definitions are
dffv2 5444 and dffv3 6171. For other alternate definitions
(that fail to
evaluate to the empty set for proper classes), see fv2 5373,
fv3 5393, and
fv4 6172. Restricted equivalents that require to be a function are
shown in funfv 5438 and funfv2 5439. For the familiar definition of function
value in terms of ordered pair membership, see funopfvb 5418.
(Contributed by NM, 1-Aug-1994.) |