Definition df-fv 3194

Description: Define the value of a function. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 3424), 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 3740 and fvprc 3716). 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 3715 and fv3 3728. Restricted equivalents that require F to be a function are shown in funfv 3765 and funfv2 3766. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 3751.

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 3178	. 2 class (F` A)
4	1	csn 2406	. . . . . 6 class {A}
5	2, 4	cima 3169	. . . . 5 class (F"{A})
6		vx	. . . . . . 7 set x
7	6	cv 954	. . . . . 6 class x
8	7	csn 2406	. . . . 5 class {x}
9	5, 8	wceq 955	. . . 4 wff (F"{A}) = {x}
10	9, 6	cab 1462	. . 3 class {x | (F"{A}) = {x}}
11	10	cuni 2499	. 2 class U.{x | (F"{A}) = {x}}
12	3, 11	wceq 955	1 wff (F` A) = U.{x | (F"{A}) = {x}}

This definition is referenced by:  fv2 3715  fvprc 3716  fveq1 3718  fveq2 3719  hbfv 3724  fvex 3727  fvres 3729  fvopabn 3781  avril1 8739

Copyright terms: Public domain