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

Definition df-fv 5279
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12446 after we define cosine in df-cos 12368). Typically, function  F is defined using maps-to notation (see df-mpt 4095 and df-mpt2 5879), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 20846). Note that df-ov 5877 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 5568 and fvprc 5535). 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 5608, dffv3 5537, fv2 5536, and fv3 5557 (the latter two previously required  A to be a set.) Restricted equivalents that require  F to be a function are shown in funfv 5602 and funfv2 5603. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5582. (Contributed 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 5271 . 2  class  ( F `
 A )
4 vx . . . . 5  set  x
54cv 1631 . . . 4  class  x
61, 5, 2wbr 4039 . . 3  wff  A F x
76, 4cio 5233 . 2  class  ( iota
x A F x )
83, 7wceq 1632 1  wff  ( F `
 A )  =  ( iota x A F x )
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5532  fveu  5533  fv2  5536  dffv3  5537  fveq1  5540  fveq2  5541  nffv  5548  csbfv12g  5551  fvex  5555  fvres  5558  tz6.12-1  5560  ovtpos  6265  fvopab5  6305  rlimdm  12041  zsum  12207  isumclim3  12238  isumshft  12314  avril1  20852  zprod  24160  fvsb  27758  dfafv2  28100  rlimdmafv  28145
  Copyright terms: Public domain W3C validator