Definition df-fv 2438

Description: Define the value of a function. Although it has roots in Definition 10.2 of [Quine] p. 65, our definition apparently does not appear in the literature but is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful. The left apostrophe notation is common in set theory and 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 more conventional alternate definitions, see fv2 2828 and fv3 2839; restricted equivalents are shown in funfv 2862 and funfv2 2863. For the familiar definition of function value in terms of ordered pair membership see funfvop 2857.

Assertion

Ref	Expression
df-fv	⊢ (F ‘A) = ∪{x∣(F “ {A}) = {x}}

Distinct variable group(s):   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 2422	. 2 class (F ‘A)
4	1	csn 1808	. . . . . 6 class {A}
5	2, 4	cima 2413	. . . . 5 class (F “ {A})
6		vx	. . . . . . 7 set x
7	6	cv 1089	. . . . . 6 class x
8	7	csn 1808	. . . . 5 class {x}
9	5, 8	wceq 1091	. . . 4 wff (F “ {A}) = {x}
10	9, 6	cab 1090	. . 3 class {x∣(F “ {A}) = {x}}
11	10	cuni 1919	. 2 class ∪{x∣(F “ {A}) = {x}}
12	3, 11	wceq 1091	1 wff (F ‘A) = ∪{x∣(F “ {A}) = {x}}

This definition is referenced by:  fv2 2828  fvprc 2829  fveq1 2831  fveq2 2832  hbfv 2837  fvex 2838  fvres 2840  fvopabn 2873

metamath.org