Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-afv Structured version   Visualization version   GIF version

Definition df-afv 44044
 Description: Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹‘𝐴) = ∅ (see df-fv 6343 and ndmfv 6688), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) (Revised by BJ/AV, 25-Aug-2022.)
Assertion
Ref Expression
df-afv (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Detailed syntax breakdown of Definition df-afv
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cF . . 3 class 𝐹
31, 2cafv 44041 . 2 class (𝐹'''𝐴)
4 vx . . . . 5 setvar 𝑥
54cv 1537 . . . 4 class 𝑥
61, 5, 2wbr 5032 . . 3 wff 𝐴𝐹𝑥
76, 4caiota 44006 . 2 class (℩'𝑥𝐴𝐹𝑥)
83, 7wceq 1538 1 wff (𝐹'''𝐴) = (℩'𝑥𝐴𝐹𝑥)
 Colors of variables: wff setvar class This definition is referenced by:  dfafv2  44056
 Copyright terms: Public domain W3C validator