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	|- ( F ''' A ) = ( iota' x A F x )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1		cA	|- A
2	1 0	cafv	|- ( F ''' A )
3		vx	|- x
4	3	cv	|- x
5	1 4 0	wbr	|- A F x
6	5 3	caiota	|- ( iota' x A F x )
7	2 6	wceq	|- ( F ''' A ) = ( iota' x A F x )