Definition df-fv 3188

Description: Define the value of a function. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 3412), 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 3730 and fvprc 3706). 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 3705 and fv3 3718. Restricted equivalents that require F to be a function are shown in funfv 3755 and funfv2 3756. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 3741.

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 3172	. 2 class (F` A)
4	1	csn 2399	. . . . . 6 class {A}
5	2, 4	cima 3163	. . . . 5 class (F"{A})
6		vx	. . . . . . 7 set x
7	6	cv 952	. . . . . 6 class x
8	7	csn 2399	. . . . 5 class {x}
9	5, 8	wceq 953	. . . 4 wff (F"{A}) = {x}
10	9, 6	cab 1456	. . 3 class {x | (F"{A}) = {x}}
11	10	cuni 2493	. 2 class U.{x | (F"{A}) = {x}}
12	3, 11	wceq 953	1 wff (F` A) = U.{x | (F"{A}) = {x}}

This definition is referenced by:  fv2 3705  fvprc 3706  fveq1 3708  fveq2 3709  hbfv 3714  fvex 3717  fvres 3719  fvopabn 3771  avril1 8723

Copyright terms: Public domain