Definition df-afv 43339

Description: Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6363 and ndmfv 6700), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) (Revised by BJ/AV, 25-Aug-2022.)

Assertion

Ref	Expression
df-afv	⊢ (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Detailed syntax breakdown of Definition df-afv

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cF	. . 3 class 𝐹
3	1, 2	cafv 43336	. 2 class (𝐹'''𝐴)
4		vx	. . . . 5 setvar 𝑥
5	4	cv 1536	. . . 4 class 𝑥
6	1, 5, 2	wbr 5066	. . 3 wff 𝐴𝐹𝑥
7	6, 4	caiota 43303	. 2 class (℩'𝑥𝐴𝐹𝑥)
8	3, 7	wceq 1537	1 wff (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥)

This definition is referenced by:  dfafv2  43351