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

Definition df-fv 5228
Description: Define the value of a function,  ( F `  A ), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12425 after we define cosine in df-cos 12347). Typically function  F is defined using maps-to notation (see df-mpt 4079 and df-mpt2 5824), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 20806). Note that df-ov 5822 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 5039), 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 5513 and fvprc 5482). 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 5553 and dffv3 6280. For other alternate definitions (that fail to evaluate to the empty set for proper classes), see fv2 5481, fv3 5501, and fv4 6281. Restricted equivalents that require  F to be a function are shown in funfv 5547 and funfv2 5548. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5527. (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 5220 . 2  class  ( F `
 A )
41csn 3640 . . . . . 6  class  { A }
52, 4cima 4690 . . . . 5  class  ( F
" { A }
)
6 vx . . . . . . 7  set  x
76cv 1622 . . . . . 6  class  x
87csn 3640 . . . . 5  class  { x }
95, 8wceq 1623 . . . 4  wff  ( F
" { A }
)  =  { x }
109, 6cab 2269 . . 3  class  { x  |  ( F " { A } )  =  { x } }
1110cuni 3827 . 2  class  U. {
x  |  ( F
" { A }
)  =  { x } }
123, 11wceq 1623 1  wff  ( F `
 A )  = 
U. { x  |  ( F " { A } )  =  {
x } }
Colors of variables: wff set class
This definition is referenced by:  fv2  5481  fvprc  5482  fveq1  5484  fveq2  5485  nffv  5492  csbfv12g  5495  csbfv12gALT  5496  fvex  5499  fvres  5502  fvco2  5555  dffv3  6280  shftval  11564  avril1  20829  repfuntw  24571  dfafv2  27406  csbfv12gALTVD  27978
  Copyright terms: Public domain W3C validator