Metamath Proof Explorer


Definition df-afv

Description: Alternative definition of the value of a function, ( F ''' A ) , also known as function application. In contrast to ( FA ) = (/) (see df-fv and ndmfv ), ( F ''' A ) = _V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017) (Revised by BJ/AV, 25-Aug-2022)

Ref Expression
Assertion df-afv F ''' A = ι

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF class F
1 cA class A
2 1 0 cafv class F ''' A
3 vx setvar x
4 3 cv setvar x
5 1 4 0 wbr wff A F x
6 5 3 caiota class ι
7 2 6 wceq wff F ''' A = ι