Description: Define the value of a
function,      ,
also known as function
application. For example,     (we prove this in cos0 12756
after we define cosine in df-cos 12678). Typically, function is
defined using maps-to notation (see df-mpt 4271 and df-mpt2 6089), but this
is not required. For example,
         
(ex-fv 21756).
Note that df-ov 6087 will define two-argument functions using
ordered pairs
as  . This
particular definition 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 5758 and fvprc 5725).
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 5799, dffv3 5727, fv2 5726,
and fv3 5747 (the latter two previously
required to be
a set.) Restricted equivalents that require
to be a function are shown in funfv 5793 and funfv2 5794. For the familiar
definition of function value in terms of ordered pair membership, see
funopfvb 5773. (Contributed by NM, 1-Aug-1994.) Revised
to use
 .
Original version is now theorem dffv4 5728. (Revised by Scott
Fenton, 6-Oct-2017.) |
