Definition df-afv2 47221

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

Assertion

Ref	Expression
df-afv2	⊢ (𝐹''''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ∪ ran 𝐹)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Detailed syntax breakdown of Definition df-afv2

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cF	. . 3 class 𝐹
3	1, 2	cafv2 47220	. 2 class (𝐹''''𝐴)
4	1, 2	wdfat 47128	. . 3 wff 𝐹 defAt 𝐴
5		vx	. . . . . 6 setvar 𝑥
6	5	cv 1539	. . . . 5 class 𝑥
7	1, 6, 2	wbr 5143	. . . 4 wff 𝐴𝐹𝑥
8	7, 5	cio 6512	. . 3 class (℩𝑥𝐴𝐹𝑥)
9	2	crn 5686	. . . . 5 class ran 𝐹
10	9	cuni 4907	. . . 4 class ∪ ran 𝐹
11	10	cpw 4600	. . 3 class 𝒫 ∪ ran 𝐹
12	4, 8, 11	cif 4525	. 2 class if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ∪ ran 𝐹)
13	3, 12	wceq 1540	1 wff (𝐹''''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ∪ ran 𝐹)

This definition is referenced by:  dfatafv2iota  47222  ndfatafv2  47223  afv2ex  47226  afv2eq12d  47227  nfafv2  47230  dfafv22  47271