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

Definition df-fv 5812
Description: Define the value of a function, (𝐹𝐴), also known as function application. For example, (cos‘0) = 1 (we prove this in cos0 14719 after we define cosine in df-cos 14640). Typically, function 𝐹 is defined using maps-to notation (see df-mpt 4645 and df-mpt2 6554), but this is not required. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9 (ex-fv 26692). Note that df-ov 6552 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 6128 and fvprc 6097). 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 6181, dffv3 6099, fv2 6098, and fv3 6116 (the latter two previously required 𝐴 to be a set.) Restricted equivalents that require 𝐹 to be a function are shown in funfv 6175 and funfv2 6176. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 6149. (Contributed by NM, 1-Aug-1994.) Revised to use . Original version is now theorem dffv4 6100. (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 class 𝐴
2 cF . . 3 class 𝐹
31, 2cfv 5804 . 2 class (𝐹𝐴)
4 vx . . . . 5 setvar 𝑥
54cv 1474 . . . 4 class 𝑥
61, 5, 2wbr 4583 . . 3 wff 𝐴𝐹𝑥
76, 4cio 5766 . 2 class (℩𝑥𝐴𝐹𝑥)
83, 7wceq 1475 1 wff (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
Colors of variables: wff setvar class
This definition is referenced by:  tz6.12-2  6094  fveu  6095  fv2  6098  dffv3  6099  fveq1  6102  fveq2  6103  nffv  6110  fvex  6113  fvres  6117  tz6.12-1  6120  csbfv12  6141  fvopab5  6217  ovtpos  7254  rlimdm  14130  zsum  14296  isumclim3  14332  isumshft  14410  zprod  14506  iprodclim3  14570  avril1  26711  uncov  32560  fvsb  37677  dfafv2  39861  rlimdmafv  39906
  Copyright terms: Public domain W3C validator