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

Definition df-fv 5465
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12756 after we define cosine in df-cos 12678). Typically, function  F is defined using maps-to notation (see df-mpt 4271 and df-mpt2 6089), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 21756). Note that df-ov 6087 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 5758 and fvprc 5725). 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 5799, dffv3 5727, fv2 5726, and fv3 5747 (the latter two previously required  A to be a set.) Restricted equivalents that require  F to be a function are shown in funfv 5793 and funfv2 5794. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5773. (Contributed by NM, 1-Aug-1994.) Revised to use  iota. Original version is now theorem dffv4 5728. (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 5457 . 2  class  ( F `
 A )
4 vx . . . . 5  set  x
54cv 1652 . . . 4  class  x
61, 5, 2wbr 4215 . . 3  wff  A F x
76, 4cio 5419 . 2  class  ( iota
x A F x )
83, 7wceq 1653 1  wff  ( F `
 A )  =  ( iota x A F x )
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5722  fveu  5723  fv2  5726  dffv3  5727  fveq1  5730  fveq2  5731  nffv  5738  csbfv12g  5741  fvex  5745  fvres  5748  tz6.12-1  5750  ovtpos  6497  fvopab5  6537  rlimdm  12350  zsum  12517  isumclim3  12548  isumshft  12624  avril1  21762  zprod  25268  iprodclim3  25318  fvsb  27645  dfafv2  27986  rlimdmafv  28031
  Copyright terms: Public domain W3C validator