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   GIF version

Definition df-dfat 41891
Description: Definition of the predicate that determines if some class 𝐹 is defined as function for an argument 𝐴 or, in other words, if the function value for some class 𝐹 for an argument 𝐴 is defined. We say that 𝐹 is defined at 𝐴 if a 𝐹 is a function restricted to the member 𝐴 of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.)
Assertion
Ref Expression
df-dfat (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))

Detailed syntax breakdown of Definition df-dfat
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cF . . 3 class 𝐹
31, 2wdfat 41888 . 2 wff 𝐹 defAt 𝐴
42cdm 5279 . . . 4 class dom 𝐹
51, 4wcel 2155 . . 3 wff 𝐴 ∈ dom 𝐹
61csn 4336 . . . . 5 class {𝐴}
72, 6cres 5281 . . . 4 class (𝐹 ↾ {𝐴})
87wfun 6064 . . 3 wff Fun (𝐹 ↾ {𝐴})
95, 8wa 384 . 2 wff (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))
103, 9wb 197 1 wff (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
Colors of variables: wff setvar class
This definition is referenced by:  dfateq12d  41898  nfdfat  41899  dfdfat2  41900  fundmdfat  41901  dfatprc  41902  dfatelrn  41903  ndmafv  41912  nfunsnafv  41914  afvpcfv0  41918  afvfvn0fveq  41922  afv0nbfvbi  41923  fnbrafvb  41926  afvelrn  41940  afvres  41944  tz6.12-afv  41945  dmfcoafv  41947  afvco2  41948  aovmpt4g  41973  ndmafv2nrn  41994  funressndmafv2rn  41995  nfunsnafv2  41997  dmafv2rnb  42001  afv2res  42011  tz6.12-afv2  42012  dfatbrafv2b  42017  dfatdmfcoafv2  42026  dfatcolem  42027  dfatco  42028  afv2ndeffv0  42032  afv2fvn0fveq  42036
  Copyright terms: Public domain W3C validator