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

Definition df-fv 5421
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12706 after we define cosine in df-cos 12628). Typically, function  F is defined using maps-to notation (see df-mpt 4228 and df-mpt2 6045), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 21704). Note that df-ov 6043 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 5714 and fvprc 5681). 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 5755, dffv3 5683, fv2 5682, and fv3 5703 (the latter two previously required  A to be a set.) Restricted equivalents that require  F to be a function are shown in funfv 5749 and funfv2 5750. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5729. (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 5413 . 2  class  ( F `
 A )
4 vx . . . . 5  set  x
54cv 1648 . . . 4  class  x
61, 5, 2wbr 4172 . . 3  wff  A F x
76, 4cio 5375 . 2  class  ( iota
x A F x )
83, 7wceq 1649 1  wff  ( F `
 A )  =  ( iota x A F x )
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5678  fveu  5679  fv2  5682  dffv3  5683  fveq1  5686  fveq2  5687  nffv  5694  csbfv12g  5697  fvex  5701  fvres  5704  tz6.12-1  5706  ovtpos  6453  fvopab5  6493  rlimdm  12300  zsum  12467  isumclim3  12498  isumshft  12574  avril1  21710  zprod  25216  iprodclim3  25266  fvsb  27522  dfafv2  27863  rlimdmafv  27908
  Copyright terms: Public domain W3C validator