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	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$$classF$$
1		cA	$$classA$$
2	1 0	cafv2	$$class\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)$$
3	1 0	wdfat	$$wffF\mathrm{defAt}A$$
4		vx	$$setvarx$$
5	4	cv	$$setvarx$$
6	1 5 0	wbr	$$wffAFx$$
7	6 4	cio	$$class\left(\iota x|AFx\right)$$
8	0	crn	$$class\mathrm{ran}F$$
9	8	cuni	$$class\bigcup \mathrm{ran}F$$
10	9	cpw	$$class𝒫\bigcup \mathrm{ran}F$$
11	3 7 10	cif	$$classif\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)$$
12	2 11	wceq	$$wff\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)$$