Definition df-fv 5341

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 4157), but this is not required. For example, 𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cF	. . 3 class 𝐹
3	1, 2	cfv 5333	. 2 class (𝐹‘𝐴)
4		vx	. . . . 5 setvar 𝑥
5	4	cv 1397	. . . 4 class 𝑥
6	1, 5, 2	wbr 4093	. . 3 wff 𝐴𝐹𝑥
7	6, 4	cio 5291	. 2 class (℩𝑥𝐴𝐹𝑥)
8	3, 7	wceq 1398	1 wff (𝐹‘𝐴) = (℩𝑥𝐴𝐹𝑥)

This definition is referenced by:  tz6.12-2  5639  fveu  5640  fv2  5643  dffv3g  5644  fveq1  5647  fveq2  5648  nffv  5658  fvss  5662  funfvex  5665  fvres  5672  tz6.12-1  5675  elfvm  5681  elfvfvex  5682  fvmbr  5683  nfvres  5684  0fv  5686  csbfv12g  5688  ovtposg  6468  zsumdc  12025  isumclim3  12064  isumshft  12131  zproddc  12220