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

Definition df-dfat 38617
Description: Definition of the predicate that determines if some class  F is defined as function for an argument  A or, in other words, if the function value for some class  F for an argument  A is defined. We say that  F is defined at  A if a  F is a function restricted to the member  A of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.)
Assertion
Ref Expression
df-dfat  |-  ( F defAt 
A  <->  ( A  e. 
dom  F  /\  Fun  ( F  |`  { A }
) ) )

Detailed syntax breakdown of Definition df-dfat
StepHypRef Expression
1 cA . . 3  class  A
2 cF . . 3  class  F
31, 2wdfat 38614 . 2  wff  F defAt  A
42cdm 4834 . . . 4  class  dom  F
51, 4wcel 1887 . . 3  wff  A  e. 
dom  F
61csn 3968 . . . . 5  class  { A }
72, 6cres 4836 . . . 4  class  ( F  |`  { A } )
87wfun 5576 . . 3  wff  Fun  ( F  |`  { A }
)
95, 8wa 371 . 2  wff  ( A  e.  dom  F  /\  Fun  ( F  |`  { A } ) )
103, 9wb 188 1  wff  ( F defAt 
A  <->  ( A  e. 
dom  F  /\  Fun  ( F  |`  { A }
) ) )
Colors of variables: wff setvar class
This definition is referenced by:  dfateq12d  38631  nfdfat  38632  dfdfat2  38633  ndmafv  38642  nfunsnafv  38644  afvpcfv0  38648  afvfvn0fveq  38652  afv0nbfvbi  38653  fnbrafvb  38656  afvelrn  38670  afvres  38674  tz6.12-afv  38675  dmfcoafv  38677  afvco2  38678  aovmpt4g  38703
  Copyright terms: Public domain W3C validator