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

Definition df-afv2 43293
 Description: Alternate definition of the value of a function, (𝐹''''𝐴), also known as function application (and called "alternate function value" in the following). In contrast to (𝐹‘𝐴) = ∅ (see comment of df-fv 6362, and especially ndmfv 6699), (𝐹''''𝐴) is guaranteed not to be in the range of 𝐹 if 𝐹 is not defined at 𝐴 (whereas ∅ can be a member of ran 𝐹). (Contributed by AV, 2-Sep-2022.)
Assertion
Ref Expression
df-afv2 (𝐹''''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ran 𝐹)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Detailed syntax breakdown of Definition df-afv2
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cF . . 3 class 𝐹
31, 2cafv2 43292 . 2 class (𝐹''''𝐴)
41, 2wdfat 43200 . . 3 wff 𝐹 defAt 𝐴
5 vx . . . . . 6 setvar 𝑥
65cv 1529 . . . . 5 class 𝑥
71, 6, 2wbr 5063 . . . 4 wff 𝐴𝐹𝑥
87, 5cio 6311 . . 3 class (℩𝑥𝐴𝐹𝑥)
92crn 5555 . . . . 5 class ran 𝐹
109cuni 4837 . . . 4 class ran 𝐹
1110cpw 4542 . . 3 class 𝒫 ran 𝐹
124, 8, 11cif 4470 . 2 class if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ran 𝐹)
133, 12wceq 1530 1 wff (𝐹''''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ran 𝐹)
 Colors of variables: wff setvar class This definition is referenced by:  dfatafv2iota  43294  ndfatafv2  43295  afv2ex  43298  afv2eq12d  43299  nfafv2  43302  dfafv22  43343
 Copyright terms: Public domain W3C validator