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

Definition df-fv 5425
Description: Define the value of a function, , also known as function application. For example, (we prove this in cos0 13220 after we define cosine in df-cos 13142). Typically, function is defined using maps-to notation (see df-mpt 4362 and df-mpt2 6072), but this is not required. For example, ={<.2,6>.,<.3,9>.}->( `3)=9 (ex-fv 22260). Note that df-ov 6070 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 5708 and fvprc 5679). 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 5757, dffv3 5681, fv2 5680, and fv3 5697 (the latter two previously required to be a set.) Restricted equivalents that require to be a function are shown in funfv 5751 and funfv2 5752. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5728. (Contributed by NM, 1-Aug-1994.) Revised to use iota. Original version is now theorem dffv4 5682. (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 5417 . 2
4 vx . . . . 5
54cv 1661 . . . 4
61, 5, 2wbr 4302 . . 3
76, 4cio 5378 . 2
83, 7wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5676  fveu  5677  fv2  5680  dffv3  5681  fveq1  5684  fveq2  5685  nffv  5692  fvex  5695  fvres  5698  tz6.12-1  5700  csbfv12  5718  csbfv12gOLD  5719  fvopab5  5787  ovtpos  6677  rlimdm  12815  zsum  12982  isumclim3  13013  isumshft  13088  avril1  22266  zprod  26093  iprodclim3  26143  fvsb  28557  dfafv2  28894  rlimdmafv  28939
  Copyright terms: Public domain W3C validator