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

Definition df-afv 27975
Description: Alternative definition of the value of a function,  ( F''' A ), also known as function application. In contrast to  ( F `  A )  =  (/) (see df-fv 5263 and ndmfv 5552),  ( 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 ,  U. { x  |  ( F " { A } )  =  {
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 27972 . 2  class  ( F''' A )
41, 2wdfat 27971 . . 3  wff  F defAt  A
51csn 3640 . . . . . . 7  class  { A }
62, 5cima 4692 . . . . . 6  class  ( F
" { A }
)
7 vx . . . . . . . 8  set  x
87cv 1622 . . . . . . 7  class  x
98csn 3640 . . . . . 6  class  { x }
106, 9wceq 1623 . . . . 5  wff  ( F
" { A }
)  =  { x }
1110, 7cab 2269 . . . 4  class  { x  |  ( F " { A } )  =  { x } }
1211cuni 3827 . . 3  class  U. {
x  |  ( F
" { A }
)  =  { x } }
13 cvv 2788 . . 3  class  _V
144, 12, 13cif 3565 . 2  class  if ( F defAt  A ,  U. { x  |  ( F " { A }
)  =  { x } } ,  _V )
153, 14wceq 1623 1  wff  ( F''' A )  =  if ( F defAt  A ,  U. { x  |  ( F " { A } )  =  {
x } } ,  _V )
Colors of variables: wff set class
This definition is referenced by:  dfafv2  27995
  Copyright terms: Public domain W3C validator