Definition df-fv 3193

Description: Define the value of a function. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 3420), 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 3736 and fvprc 3712). 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 3711 and fv3 3724. Restricted equivalents that require F to be a function are shown in funfv 3761 and funfv2 3762. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 3747.

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 3177	. 2 class (F` A)
4	1	csn 2405	. . . . . 6 class {A}
5	2, 4	cima 3168	. . . . 5 class (F"{A})
6		vx	. . . . . . 7 set x
7	6	cv 953	. . . . . 6 class x
8	7	csn 2405	. . . . 5 class {x}
9	5, 8	wceq 954	. . . 4 wff (F"{A}) = {x}
10	9, 6	cab 1461	. . 3 class {x | (F"{A}) = {x}}
11	10	cuni 2498	. 2 class U.{x | (F"{A}) = {x}}
12	3, 11	wceq 954	1 wff (F` A) = U.{x | (F"{A}) = {x}}

This definition is referenced by:  fv2 3711  fvprc 3712  fveq1 3714  fveq2 3715  hbfv 3720  fvex 3723  fvres 3725  fvopabn 3777  avril1 8723

Copyright terms: Public domain