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

Definition df-fv 5545
Description: Define the value of a function, , also known as function application. For example, (we prove this in cos0 13592 after we define cosine in df-cos 13514). Typically, function is defined using maps-to notation (see df-mpt 4469 and df-mpt2 6227), but this is not required. For example, ={<.2,6>.,<.3,9>.}->( `3)=9 (ex-fv 24119). Note that df-ov 6225 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 5837 and fvprc 5807). 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 5887, dffv3 5809, fv2 5808, and fv3 5826 (the latter two previously required to be a set.) Restricted equivalents that require to be a function are shown in funfv 5881 and funfv2 5882. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5858. (Contributed by NM, 1-Aug-1994.) Revised to use iota. Original version is now theorem dffv4 5810. (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 5537 . 2
4 vx . . . . 5
54cv 1369 . . . 4
61, 5, 2wbr 4409 . . 3
76, 4cio 5498 . 2
83, 7wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  tz6.12-2  5804  fveu  5805  fv2  5808  dffv3  5809  fveq1  5812  fveq2  5813  nffv  5820  fvex  5823  fvres  5827  tz6.12-1  5829  csbfv12  5848  csbfv12gOLD  5849  fvopab5  5918  ovtpos  6894  rlimdm  13187  zsum  13353  isumclim3  13384  isumshft  13460  avril1  24125  zprod  27906  iprodclim3  27956  fvsb  30168  dfafv2  30915  rlimdmafv  30960
  Copyright terms: Public domain W3C validator