Users' Mathboxes 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 40501
Description: Alternative definition of the value of a function, (𝐹'''𝐴), also known as function application. In contrast to (𝐹𝐴) = ∅ (see df-fv 5855 and ndmfv 6175), (𝐹'''𝐴) = V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.)
Assertion
Ref Expression
df-afv (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), V)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Detailed syntax breakdown of Definition df-afv
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cF . . 3 class 𝐹
31, 2cafv 40498 . 2 class (𝐹'''𝐴)
41, 2wdfat 40497 . . 3 wff 𝐹 defAt 𝐴
5 vx . . . . . 6 setvar 𝑥
65cv 1479 . . . . 5 class 𝑥
71, 6, 2wbr 4613 . . . 4 wff 𝐴𝐹𝑥
87, 5cio 5808 . . 3 class (℩𝑥𝐴𝐹𝑥)
9 cvv 3186 . . 3 class V
104, 8, 9cif 4058 . 2 class if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), V)
113, 10wceq 1480 1 wff (𝐹'''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), V)
Colors of variables: wff setvar class
This definition is referenced by:  dfafv2  40516
  Copyright terms: Public domain W3C validator