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

Definition df-fv 5509
Description: Define the value of a function, , also known as function ?Error: cos ` 0 ) = 1 ^^^ This math symbol is not active (i.e. was not declared in this scope). application. For example, ( `0)=1 (we prove this in cos0 12802 after we define cosine in df-cos 12724). Typically, function is defined using maps-to notation (see df-mpt 4303 and df-mpt2 6134), but this is not required. For example, ?Error: 2 , 6 >. , <. 3 , 9 >. } -> ( F ` 3 ) = 9 ^ This math symbol is not active (i.e. was not declared in this scope). ={<.2,6>.,<.3,9>.}->( `3)=9 (ex-fv 21802). Note that df-ov 6132 will define two-argument functions using ordered pairs as . 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 5798 and fvprc 5769). 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 ( ) notation for a function's value at , i.e. " of ," but without context-dependent notational ambiguity. Alternate definitions are dffv2 5844, dffv3 5771, fv2 5770, and fv3 5787 (the latter two previously required to be a set.) Restricted equivalents that require to be a function are shown in funfv 5838 and funfv2 5839. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5818. (Contributed by NM, 1-Aug-1994.) Revised to use iota. Original version is now theorem dffv4 5772. (Revised by Scott Fenton, 6-Oct-2017.)
Assertion
Ref Expression
df-fv
Distinct variable groups:   ,   ,

Detailed syntax breakdown of Definition df-fv
StepHypRef Expression
1 cA . . 3
2 cF . . 3
31, 2cfv 5501 . 2
4 vx . . . . 5
54cv 1653 . . . 4
61, 5, 2wbr 4243 . . 3
76, 4cio 5462 . 2
83, 7wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5766  fveu  5767  fv2  5770  dffv3  5771  fveq1  5774  fveq2  5775  nffv  5782  fvex  5785  fvres  5788  tz6.12-1  5790  csbfv12  5808  csbfv12gOLD  5809  ovtpos  6544  fvopab5  6584  rlimdm  12396  zsum  12563  isumclim3  12594  isumshft  12670  avril1  21808  zprod  25367  iprodclim3  25417  fvsb  27810  dfafv2  28151  rlimdmafv  28196
  Copyright terms: Public domain W3C validator