Definition df-fv 3196

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

Assertion

Ref	Expression
df-fv	⊢ (F ‘A) = ∪{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 3180	. 2 class (F ‘A)
4	1	csn 2407	. . . . . 6 class {A}
5	2, 4	cima 3171	. . . . 5 class (F “ {A})
6		vx	. . . . . . 7 set x
7	6	cv 955	. . . . . 6 class x
8	7	csn 2407	. . . . 5 class {x}
9	5, 8	wceq 956	. . . 4 wff (F “ {A}) = {x}
10	9, 6	cab 1463	. . 3 class {x∣(F “ {A}) = {x}}
11	10	cuni 2501	. 2 class ∪{x∣(F “ {A}) = {x}}
12	3, 11	wceq 956	1 wff (F ‘A) = ∪{x∣(F “ {A}) = {x}}

This definition is referenced by:  fv2 3718  fvprc 3719  fveq1 3721  fveq2 3722  hbfv 3727  fvex 3730  fvres 3732  fvopabn 3784  avril1 8739

Copyright terms: Public domain