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

Definition df-fv 5601
 Description: Define the value of a function, , also known as function application. For example, (we prove this in cos0 13885 after we define cosine in df-cos 13806). Typically, function is defined using maps-to notation (see df-mpt 4512 and df-mpt2 6301), but this is not required. For example, ={<.2,6>.,<.3,9>.}->( 3)=9 (ex-fv 25164). Note that df-ov 6299 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 5895 and fvprc 5865). 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 5946, dffv3 5867, fv2 5866, and fv3 5884 (the latter two previously required to be a set.) Restricted equivalents that require to be a function are shown in funfv 5940 and funfv2 5941. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5916. (Contributed by NM, 1-Aug-1994.) Revised to use iota`. Original version is now theorem dffv4 5868. (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 5593 . 2
4 vx . . . . 5
54cv 1394 . . . 4
61, 5, 2wbr 4452 . . 3
76, 4cio 5554 . 2
83, 7wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  tz6.12-2  5862  fveu  5863  fv2  5866  dffv3  5867  fveq1  5870  fveq2  5871  nffv  5878  fvex  5881  fvres  5885  tz6.12-1  5887  csbfv12  5906  csbfv12gOLD  5907  fvopab5  5979  ovtpos  6989  rlimdm  13374  zsum  13540  isumclim3  13574  isumshft  13651  zprod  13744  iprodclim3  13793  avril1  25171  fvsb  31361  dfafv2  32217  rlimdmafv  32262
 Copyright terms: Public domain W3C validator