Definition df-fv 5266

Description: Define the value of a function, ( F ` A ), also known as function application. For example, ( _I ` (/) ) = (/). Typically, function F is defined using maps-to notation (see df-mpt 4096), 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 F B ) = ( F ` <. 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 F ( A ) notation for a function's value at A, i.e., " F of A," but without context-dependent notational ambiguity. (Contributed by NM, 1-Aug-1994.) Revised to use iota. (Revised by Scott Fenton, 6-Oct-2017.)

Assertion

Ref	Expression
df-fv	|- ( F ` A ) = ( iota x A F x )

Distinct variable groups:   x, A   x, F

Detailed syntax breakdown of Definition df-fv

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cF	. . 3 class F
3	1, 2	cfv 5258	. 2 class ( F ` A )
4		vx	. . . . 5 setvar x
5	4	cv 1363	. . . 4 class x
6	1, 5, 2	wbr 4033	. . 3 wff A F x
7	6, 4	cio 5217	. 2 class ( iota x A F x )
8	3, 7	wceq 1364	1 wff ( F ` A ) = ( iota x A F x )

This definition is referenced by:  tz6.12-2  5549  fveu  5550  fv2  5553  dffv3g  5554  fveq1  5557  fveq2  5558  nffv  5568  fvss  5572  funfvex  5575  fvres  5582  tz6.12-1  5585  elfvm  5591  nfvres  5592  0fv  5594  csbfv12g  5596  ovtposg  6317  zsumdc  11549  isumclim3  11588  isumshft  11655  zproddc  11744