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

Definition df-fv 4654
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12357 after we define cosine in df-cos 12279). Typically function  F is defined using maps-to notation (see df-mpt 4019 and df-mpt2 5762), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 20738). Note that df-ov 5760 will define two-argument functions using ordered pairs as  ( A F B )  =  ( F `  <. A ,  B >. ). Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 4994), our definition apparently does not appear in the literature. However, it 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 5451 and fvprc 5420). 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 5491 and dffv3 6218. For other alternate definitions (that fail to evaluate to the empty set for proper classes), see fv2 5419, fv3 5439, and fv4 6219. Restricted equivalents that require  F to be a function are shown in funfv 5485 and funfv2 5486. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5465. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fv  |-  ( F `
 A )  = 
U. { x  |  ( F " { A } )  =  {
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 4638 . 2  class  ( F `
 A )
41csn 3581 . . . . . 6  class  { A }
52, 4cima 4629 . . . . 5  class  ( F
" { A }
)
6 vx . . . . . . 7  set  x
76cv 1618 . . . . . 6  class  x
87csn 3581 . . . . 5  class  { x }
95, 8wceq 1619 . . . 4  wff  ( F
" { A }
)  =  { x }
109, 6cab 2242 . . 3  class  { x  |  ( F " { A } )  =  { x } }
1110cuni 3768 . 2  class  U. {
x  |  ( F
" { A }
)  =  { x } }
123, 11wceq 1619 1  wff  ( F `
 A )  = 
U. { x  |  ( F " { A } )  =  {
x } }
Colors of variables: wff set class
This definition is referenced by:  fv2  5419  fvprc  5420  fveq1  5422  fveq2  5423  nffv  5430  csbfv12g  5433  csbfv12gALT  5434  fvex  5437  fvres  5440  fvco2  5493  dffv3  6218  shftval  11499  avril1  20761  repfuntw  24492  csbfv12gALTVD  27688
  Copyright terms: Public domain W3C validator