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	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\iota$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1		cA	$$classA$$
2	1 0	cafv	$$class\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	1 4 0	wbr	$$wffAFx$$
6	5 3	caiota	$$class\iota$$
7	2 6	wceq	$$wff\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=\iota$$