MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fv Structured version   Unicode version

Definition df-fv 5454
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12743 after we define cosine in df-cos 12665). Typically, function  F is defined using maps-to notation (see df-mpt 4260 and df-mpt2 6078), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 21743). Note that df-ov 6076 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 5747 and fvprc 5714). 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 5788, dffv3 5716, fv2 5715, and fv3 5736 (the latter two previously required  A to be a set.) Restricted equivalents that require  F to be a function are shown in funfv 5782 and funfv2 5783. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5762. (Contributed by NM, 1-Aug-1994.) Revised to use  iota. Original version is now theorem dffv4 5717. (Revised by Scott Fenton, 6-Oct-2017.)
Assertion
Ref Expression
df-fv  |-  ( F `
 A )  =  ( iota x A F x )
Distinct variable groups:    x, A    x, F

Detailed syntax breakdown of Definition df-fv
StepHypRef Expression
1 cA . . 3  class  A
2 cF . . 3  class  F
31, 2cfv 5446 . 2  class  ( F `
 A )
4 vx . . . . 5  set  x
54cv 1651 . . . 4  class  x
61, 5, 2wbr 4204 . . 3  wff  A F x
76, 4cio 5408 . 2  class  ( iota
x A F x )
83, 7wceq 1652 1  wff  ( F `
 A )  =  ( iota x A F x )
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5711  fveu  5712  fv2  5715  dffv3  5716  fveq1  5719  fveq2  5720  nffv  5727  csbfv12g  5730  fvex  5734  fvres  5737  tz6.12-1  5739  ovtpos  6486  fvopab5  6526  rlimdm  12337  zsum  12504  isumclim3  12535  isumshft  12611  avril1  21749  zprod  25255  iprodclim3  25305  fvsb  27612  dfafv2  27953  rlimdmafv  27998
  Copyright terms: Public domain W3C validator