ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fv Unicode version

Definition df-fv 5206
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  (  _I  `  (/) )  =  (/). Typically, function  F is defined using maps-to notation (see df-mpt 4052), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9. We will later 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. 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. (Contributed by NM, 1-Aug-1994.) Revised to use  iota. (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 5198 . 2  class  ( F `
 A )
4 vx . . . . 5  setvar  x
54cv 1347 . . . 4  class  x
61, 5, 2wbr 3989 . . 3  wff  A F x
76, 4cio 5158 . 2  class  ( iota
x A F x )
83, 7wceq 1348 1  wff  ( F `
 A )  =  ( iota x A F x )
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5487  fveu  5488  fv2  5491  dffv3g  5492  fveq1  5495  fveq2  5496  nffv  5506  fvss  5510  funfvex  5513  fvres  5520  tz6.12-1  5523  nfvres  5529  0fv  5531  csbfv12g  5532  ovtposg  6238  zsumdc  11347  isumclim3  11386  isumshft  11453  zproddc  11542
  Copyright terms: Public domain W3C validator