Definition df-fv 4796

Description: Define the value of a function. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-fv	⊢ (F ‘A) = (℩xAFx)

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 4782	. 2 class (F ‘A)
4		vx	. . . . 5 setvar x
5	4	cv 1641	. . . 4 class x
6	1, 5, 2	wbr 4640	. . 3 wff AFx
7	6, 4	cio 4338	. 2 class (℩xAFx)
8	3, 7	wceq 1642	1 wff (F ‘A) = (℩xAFx)

This definition is referenced by:  fv2  5325  fvprc  5326  fveq1  5328  fveq2  5329  nffv  5335  csbfv12g  5337  fvex  5340  fvres  5343  tz6.12-1  5345  fvco2  5383