ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fv GIF version

Definition df-fv 5101
Description: Define the value of a function, (𝐹𝐴), also known as function application. For example, ( I ‘∅) = ∅. Typically, function 𝐹 is defined using maps-to notation (see df-mpt 3961), but this is not required. For example, F = { 2 , 6 , 3 , 9 } -> ( F 3 ) = 9 . We will later 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. 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. (Contributed by NM, 1-Aug-1994.) Revised to use . (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 5093 . 2 class (𝐹𝐴)
4 vx . . . . 5 setvar 𝑥
54cv 1315 . . . 4 class 𝑥
61, 5, 2wbr 3899 . . 3 wff 𝐴𝐹𝑥
76, 4cio 5056 . 2 class (℩𝑥𝐴𝐹𝑥)
83, 7wceq 1316 1 wff (𝐹𝐴) = (℩𝑥𝐴𝐹𝑥)
Colors of variables: wff set class
This definition is referenced by:  tz6.12-2  5380  fveu  5381  fv2  5384  dffv3g  5385  fveq1  5388  fveq2  5389  nffv  5399  fvss  5403  funfvex  5406  fvres  5413  tz6.12-1  5416  nfvres  5422  0fv  5424  csbfv12g  5425  ovtposg  6124  zsumdc  11108  isumclim3  11147  isumshft  11214
  Copyright terms: Public domain W3C validator