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

Definition df-fv 5446
Description: Define the value of a function, , also known as function application. For example, (we prove this in cos0 13281 after we define cosine in df-cos 13203). Typically, function is defined using maps-to notation (see df-mpt 4378 and df-mpt2 6108), but this is not required. For example, ={<.2,6>.,<.3,9>.}->( `3)=9 (ex-fv 22772). Note that df-ov 6106 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 5731 and fvprc 5702). 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 (A) notation for a function's value at , i.e. " of ," but without context-dependent notational ambiguity. Alternate definitions are dffv2 5780, dffv3 5704, fv2 5703, and fv3 5720 (the latter two previously required to be a set.) Restricted equivalents that require to be a function are shown in funfv 5774 and funfv2 5775. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5751. (Contributed by NM, 1-Aug-1994.) Revised to use iota. Original version is now theorem dffv4 5705. (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 5438 . 2
4 vx . . . . 5
54cv 1669 . . . 4
61, 5, 2wbr 4318 . . 3
76, 4cio 5399 . 2
83, 7wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5699  fveu  5700  fv2  5703  dffv3  5704  fveq1  5707  fveq2  5708  nffv  5715  fvex  5718  fvres  5721  tz6.12-1  5723  csbfv12  5741  csbfv12gOLD  5742  fvopab5  5811  ovtpos  6726  rlimdm  12876  zsum  13043  isumclim3  13074  isumshft  13149  avril1  22778  zprod  26602  iprodclim3  26652  fvsb  28882  dfafv2  29217  rlimdmafv  29262
  Copyright terms: Public domain W3C validator