# Metamath Proof Explorer

## 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}|{A}{F}{x}\right),𝒫\bigcup \mathrm{ran}{F}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cF ${class}{F}$
1 cA ${class}{A}$
2 1 0 cafv2 ${class}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)$
3 1 0 wdfat ${wff}{F}\mathrm{defAt}{A}$
4 vx ${setvar}{x}$
5 4 cv ${setvar}{x}$
6 1 5 0 wbr ${wff}{A}{F}{x}$
7 6 4 cio ${class}\left(\iota {x}|{A}{F}{x}\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 ${class}if\left({F}\mathrm{defAt}{A},\left(\iota {x}|{A}{F}{x}\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}|{A}{F}{x}\right),𝒫\bigcup \mathrm{ran}{F}\right)$