Definition df-afv

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		cA	⊢ 𝐴
2	1 0	cafv	⊢ ( 𝐹 ''' 𝐴 )
3		vx	⊢ 𝑥
4	3	cv	⊢ 𝑥
5	1 4 0	wbr	⊢ 𝐴 𝐹 𝑥
6	5 3	caiota	⊢ ( ℩' 𝑥 𝐴 𝐹 𝑥 )
7	2 6	wceq	⊢ ( 𝐹 ''' 𝐴 ) = ( ℩' 𝑥 𝐴 𝐹 𝑥 )