Definition df-afv2

Description: Alternate definition of the value of a function, ( F '''' A ) , also known as function application (and called "alternate function value" in the following). In contrast to ( FA ) = (/) (see comment of df-fv , and especially ndmfv ), ( F '''' A ) is guaranteed not to be in the range of F if F is not defined at A (whereas (/) can be a member of ran F ). (Contributed by AV, 2-Sep-2022)

	Ref	Expression
Assertion	df-afv2	|- ( F '''' A ) = if ( F defAt A , ( iota x A F x ) , ~P U. ran F )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1		cA	|- A
2	1 0	cafv2	|- ( F '''' A )
3	1 0	wdfat	|- F defAt A
4		vx	|- x
5	4	cv	|- x
6	1 5 0	wbr	|- A F x
7	6 4	cio	|- ( iota x A F x )
8	0	crn	|- ran F
9	8	cuni	|- U. ran F
10	9	cpw	|- ~P U. ran F
11	3 7 10	cif	|- if ( F defAt A , ( iota x A F x ) , ~P U. ran F )
12	2 11	wceq	|- ( F '''' A ) = if ( F defAt A , ( iota x A F x ) , ~P U. ran F )