Description: Define the value of a function, ( FA ) , also known as function
application. For example, ( cos0 ) = 1 (we prove this in cos0 after we define cosine in df-cos ). Typically, function F is
defined using maps-to notation (see df-mpt and df-mpo ), but this is
not required. For example,
F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ( F3 ) = 9 ( ex-fv ).
Note that df-ov will define two-argument functions using ordered pairs
as ( A F B ) = ( F<. A , B >. ) . 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 and fvprc ).
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 F ( A ) notation for a
function's value at A , i.e., " F of A ", but without
context-dependent notational ambiguity. Alternate definitions are
dffv2 , dffv3 , fv2 , and fv3 (the latter two previously
required A to be a set.) Restricted equivalents that require F
to be a function are shown in funfv and funfv2 . For the familiar
definition of function value in terms of ordered pair membership, see
funopfvb . (Contributed by NM, 1-Aug-1994) Revised to use
iota . Original version is now Theorem dffv4 . (Revised by Scott
Fenton, 6-Oct-2017)