Definition df-fv 3279

Description: Define the value of a function. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 3520), our definition apparently does not appear in the literature; but 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 3856 and fvprc 3832). 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 ambiguity. For conventional alternate definitions (that fail to evaluate to the empty set for proper classes), see fv2 3831 and fv3 3844. Restricted equivalents that require F to be a function are shown in funfv 3881 and funfv2 3882. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 3867.

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 3263	. 2 class (F` A)
4	1	csn 2467	. . . . . 6 class {A}
5	2, 4	cima 3254	. . . . 5 class (F"{A})
6		vx	. . . . . . 7 set x
7	6	cv 991	. . . . . 6 class x
8	7	csn 2467	. . . . 5 class {x}
9	5, 8	wceq 992	. . . 4 wff (F"{A}) = {x}
10	9, 6	cab 1505	. . 3 class {x | (F"{A}) = {x}}
11	10	cuni 2569	. 2 class U.{x | (F"{A}) = {x}}
12	3, 11	wceq 992	1 wff (F` A) = U.{x | (F"{A}) = {x}}

This definition is referenced by:  fv2 3831  fvprc 3832  fveq1 3834  fveq2 3835  hbfv 3840  fvex 3843  fvres 3845  fvopabn 3897  avril1 9058

Copyright terms: Public domain