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

Definition df-afv 30018
Description: Alternative definition of the value of a function,  ( F''' A ), also known as function application. In contrast to  ( F `  A )  =  (/) (see df-fv 5424 and ndmfv 5712),  ( F''' A )  =  _V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.)
Assertion
Ref Expression
df-afv  |-  ( F''' A )  =  if ( F defAt  A , 
( iota x A F x ) ,  _V )
Distinct variable groups:    x, A    x, F

Detailed syntax breakdown of Definition df-afv
StepHypRef Expression
1 cA . . 3  class  A
2 cF . . 3  class  F
31, 2cafv 30015 . 2  class  ( F''' A )
41, 2wdfat 30014 . . 3  wff  F defAt  A
5 vx . . . . . 6  setvar  x
65cv 1368 . . . . 5  class  x
71, 6, 2wbr 4290 . . . 4  wff  A F x
87, 5cio 5377 . . 3  class  ( iota
x A F x )
9 cvv 2970 . . 3  class  _V
104, 8, 9cif 3789 . 2  class  if ( F defAt  A ,  ( iota x A F x ) ,  _V )
113, 10wceq 1369 1  wff  ( F''' A )  =  if ( F defAt  A , 
( iota x A F x ) ,  _V )
Colors of variables: wff setvar class
This definition is referenced by:  dfafv2  30035
  Copyright terms: Public domain W3C validator