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	⊢ ( 𝐹 '''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ∪ ran 𝐹 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		cA	⊢ 𝐴
2	1 0	cafv2	⊢ ( 𝐹 '''' 𝐴 )
3	1 0	wdfat	⊢ 𝐹 defAt 𝐴
4		vx	⊢ 𝑥
5	4	cv	⊢ 𝑥
6	1 5 0	wbr	⊢ 𝐴 𝐹 𝑥
7	6 4	cio	⊢ ( ℩ 𝑥 𝐴 𝐹 𝑥 )
8	0	crn	⊢ ran 𝐹
9	8	cuni	⊢ ∪ ran 𝐹
10	9	cpw	⊢ 𝒫 ∪ ran 𝐹
11	3 7 10	cif	⊢ if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ∪ ran 𝐹 )
12	2 11	wceq	⊢ ( 𝐹 '''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( ℩ 𝑥 𝐴 𝐹 𝑥 ) , 𝒫 ∪ ran 𝐹 )