Definition df-fv 4689

Description: Define the value of a function, ( F ` A ), also known as function application. For example, ( cos ` 0 ) = 1 (we prove this in cos0 12393 after we define cosine in df-cos 12315). Typically function F is defined using maps-to notation (see df-mpt 4053 and df-mpt2 5797), but this is not required. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ( F ` 3 ) = 9 (ex-fv 20774). Note that df-ov 5795 will define two-argument functions using ordered pairs as ( A F B ) = ( F ` <. A , B >. ). Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 5029), our definition apparently does not appear in the literature. However, it 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 5486 and fvprc 5455). 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. Alternate definitions are dffv2 5526 and dffv3 6253. For other alternate definitions (that fail to evaluate to the empty set for proper classes), see fv2 5454, fv3 5474, and fv4 6254. Restricted equivalents that require F to be a function are shown in funfv 5520 and funfv2 5521. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5500. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-fv	|- ( F ` A ) = U. { x | ( F " { A } ) = { 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 4673	. 2 class ( F ` A )
4	1	csn 3614	. . . . . 6 class { A }
5	2, 4	cima 4664	. . . . 5 class ( F " { A } )
6		vx	. . . . . . 7 set x
7	6	cv 1618	. . . . . 6 class x
8	7	csn 3614	. . . . 5 class { x }
9	5, 8	wceq 1619	. . . 4 wff ( F " { A } ) = { x }
10	9, 6	cab 2244	. . 3 class { x | ( F " { A } ) = { x } }
11	10	cuni 3801	. 2 class U. { x | ( F " { A } ) = { x } }
12	3, 11	wceq 1619	1 wff ( F ` A ) = U. { x | ( F " { A } ) = { x } }

This definition is referenced by:  fv2  5454  fvprc  5455  fveq1  5457  fveq2  5458  nffv  5465  csbfv12g  5468  csbfv12gALT  5469  fvex  5472  fvres  5475  fvco2  5528  dffv3  6253  shftval  11535  avril1  20797  repfuntw  24528  csbfv12gALTVD  27808