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

Definition df-fv 5366
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12638 after we define cosine in df-cos 12560). Typically, function  F is defined using maps-to notation (see df-mpt 4181 and df-mpt2 5986), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 21262). Note that df-ov 5984 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 5659 and fvprc 5626). 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 5699, dffv3 5628, fv2 5627, and fv3 5648 (the latter two previously required  A to be a set.) Restricted equivalents that require  F to be a function are shown in funfv 5693 and funfv2 5694. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5673. (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 5358 . 2  class  ( F `
 A )
4 vx . . . . 5  set  x
54cv 1646 . . . 4  class  x
61, 5, 2wbr 4125 . . 3  wff  A F x
76, 4cio 5320 . 2  class  ( iota
x A F x )
83, 7wceq 1647 1  wff  ( F `
 A )  =  ( iota x A F x )
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5623  fveu  5624  fv2  5627  dffv3  5628  fveq1  5631  fveq2  5632  nffv  5639  csbfv12g  5642  fvex  5646  fvres  5649  tz6.12-1  5651  ovtpos  6391  fvopab5  6431  rlimdm  12232  zsum  12399  isumclim3  12430  isumshft  12506  avril1  21268  zprod  24832  iprodclim3  24875  fvsb  27246  dfafv2  27588  rlimdmafv  27633
  Copyright terms: Public domain W3C validator