| 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 | ||
| 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.) |
| Ref | Expression |
|---|---|
| df-dfat | ⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cF | . . 3 class 𝐹 | |
| 3 | 1, 2 | wdfat 47128 | . 2 wff 𝐹 defAt 𝐴 |
| 4 | 2 | cdm 5685 | . . . 4 class dom 𝐹 |
| 5 | 1, 4 | wcel 2108 | . . 3 wff 𝐴 ∈ dom 𝐹 |
| 6 | 1 | csn 4626 | . . . . 5 class {𝐴} |
| 7 | 2, 6 | cres 5687 | . . . 4 class (𝐹 ↾ {𝐴}) |
| 8 | 7 | wfun 6555 | . . 3 wff Fun (𝐹 ↾ {𝐴}) |
| 9 | 5, 8 | wa 395 | . 2 wff (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) |
| 10 | 3, 9 | wb 206 | 1 wff (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfateq12d 47138 nfdfat 47139 dfdfat2 47140 fundmdfat 47141 dfatprc 47142 dfatelrn 47143 ndmafv 47152 nfunsnafv 47154 afvpcfv0 47158 afvfvn0fveq 47162 afv0nbfvbi 47163 fnbrafvb 47166 afvelrn 47180 afvres 47184 tz6.12-afv 47185 dmfcoafv 47187 afvco2 47188 aovmpt4g 47213 ndmafv2nrn 47234 funressndmafv2rn 47235 nfunsnafv2 47237 dmafv2rnb 47241 afv2res 47251 tz6.12-afv2 47252 dfatbrafv2b 47257 dfatdmfcoafv2 47266 dfatcolem 47267 dfatco 47268 afv2ndeffv0 47272 afv2fvn0fveq 47276 |
| Copyright terms: Public domain | W3C validator |