Definition df-afv 31624

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

Assertion

Ref	Expression
df-afv	|- ( F''' A ) = if ( F defAt A , ( iota x A F x ) , _V )

Distinct variable groups:   x, A   x, F

Detailed syntax breakdown of Definition df-afv

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cF	. . 3 class F
3	1, 2	cafv 31621	. 2 class ( F''' A )
4	1, 2	wdfat 31620	. . 3 wff F defAt A
5		vx	. . . . . 6 setvar x
6	5	cv 1373	. . . . 5 class x
7	1, 6, 2	wbr 4440	. . . 4 wff A F x
8	7, 5	cio 5540	. . 3 class ( iota x A F x )
9		cvv 3106	. . 3 class _V
10	4, 8, 9	cif 3932	. 2 class if ( F defAt A , ( iota x A F x ) , _V )
11	3, 10	wceq 1374	1 wff ( F''' A ) = if ( F defAt A , ( iota x A F x ) , _V )

This definition is referenced by:  dfafv2  31639