Users' Mathboxes 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 42059
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 6109, and especially ndmfv 6441), (𝐹''''𝐴) 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 42058 . 2 class (𝐹''''𝐴)
41, 2wdfat 41966 . . 3 wff 𝐹 defAt 𝐴
5 vx . . . . . 6 setvar 𝑥
65cv 1652 . . . . 5 class 𝑥
71, 6, 2wbr 4843 . . . 4 wff 𝐴𝐹𝑥
87, 5cio 6062 . . 3 class (℩𝑥𝐴𝐹𝑥)
92crn 5313 . . . . 5 class ran 𝐹
109cuni 4628 . . . 4 class ran 𝐹
1110cpw 4349 . . 3 class 𝒫 ran 𝐹
124, 8, 11cif 4277 . 2 class if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ran 𝐹)
133, 12wceq 1653 1 wff (𝐹''''𝐴) = if(𝐹 defAt 𝐴, (℩𝑥𝐴𝐹𝑥), 𝒫 ran 𝐹)
Colors of variables: wff setvar class
This definition is referenced by:  dfatafv2iota  42060  ndfatafv2  42061  afv2ex  42064  afv2eq12d  42065  nfafv2  42068  dfafv22  42109
  Copyright terms: Public domain W3C validator