Definition df-afv 39846

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

Assertion

Ref	Expression
df-afv	⊢ (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), V)

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 39843	. 2 class (𝐹'''𝐴)
4	1, 2	wdfat 39842	. . 3 wff 𝐹 defAt 𝐴
5		vx	. . . . . 6 setvar 𝑥
6	5	cv 1474	. . . . 5 class 𝑥
7	1, 6, 2	wbr 4583	. . . 4 wff 𝐴𝐹𝑥
8	7, 5	cio 5766	. . 3 class (℩𝑥𝐴𝐹𝑥)
9		cvv 3173	. . 3 class V
10	4, 8, 9	cif 4036	. 2 class if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), V)
11	3, 10	wceq 1475	1 wff (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), V)

This definition is referenced by:  dfafv2  39861