Definition df-fv 4147

Description: Define the value of a function. Although based on the idea embodied by Definition 10.2 of [Quine] p. 65 (see args 4411), 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 4788 and fvprc 4762). 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. Alternate definitions are dffv2 4820 and dffv3 5247. For other alternate definitions (that fail to evaluate to the empty set for proper classes), see fv2 4761, fv3 4779, and fv4 5248. Restricted equivalents that require F to be a function are shown in funfv 4816 and funfv2 4817. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 4801.

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 4131	. 2 class (F` A)
4	1	csn 3238	. . . . . 6 class {A}
5	2, 4	cima 4122	. . . . 5 class (F"{A})
6		vx	. . . . . . 7 set x
7	6	cv 1585	. . . . . 6 class x
8	7	csn 3238	. . . . 5 class {x}
9	5, 8	wceq 1586	. . . 4 wff (F"{A}) = {x}
10	9, 6	cab 2128	. . 3 class {x | (F"{A}) = {x}}
11	10	cuni 3366	. 2 class U.{x | (F"{A}) = {x}}
12	3, 11	wceq 1586	1 wff (F` A) = U.{x | (F"{A}) = {x}}

This definition is referenced by:  fv2 4761  fvprc 4762  fveq1 4764  fveq2 4765  hbfv 4771  csbfv12gALT 4775  fvex 4778  fvres 4780  fvopabn 4835  dffv3 5247  avril1 11013  repfuntw 15241  csbfv12gALTVD 17557

Copyright terms: Public domain