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

Definition df-fv 4833
 Description: Define the value of a function, (𝐹‘A), also known as function application. For example, ( I ‘∅) = ∅. Typically, function 𝐹 is defined using maps-to notation (see df-mpt 3790), 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 (A𝐹B) = (𝐹‘⟨A, B⟩). 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 𝐹(A) notation for a function's value at A, i.e. "𝐹 of A," 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 (𝐹A) = (℩xA𝐹x)
Distinct variable groups:   x,A   x,𝐹

Detailed syntax breakdown of Definition df-fv
StepHypRef Expression
1 cA . . 3 class A
2 cF . . 3 class 𝐹
31, 2cfv 4825 . 2 class (𝐹A)
4 vx . . . . 5 setvar x
54cv 1225 . . . 4 class x
61, 5, 2wbr 3734 . . 3 wff A𝐹x
76, 4cio 4788 . 2 class (℩xA𝐹x)
83, 7wceq 1226 1 wff (𝐹A) = (℩xA𝐹x)
 Colors of variables: wff set class This definition is referenced by:  tz6.12-2  5090  fveu  5091  fv2  5094  dffv3g  5095  fveq1  5098  fveq2  5099  nffv  5106  fvss  5110  funfvex  5113  fvres  5119  tz6.12-1  5121  nfvres  5127  0fv  5129  csbfv12g  5130  ovtposg  5792
 Copyright terms: Public domain W3C validator