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 |
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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cF | . . 3 | |
3 | 1, 2 | wdfat 41193 | . 2 defAt |
4 | 2 | cdm 5114 | . . . 4 |
5 | 1, 4 | wcel 1990 | . . 3 |
6 | 1 | csn 4177 | . . . . 5 |
7 | 2, 6 | cres 5116 | . . . 4 |
8 | 7 | wfun 5882 | . . 3 |
9 | 5, 8 | wa 384 | . 2 |
10 | 3, 9 | wb 196 | 1 defAt |
Colors of variables: wff setvar class |
This definition is referenced by: dfateq12d 41209 nfdfat 41210 dfdfat2 41211 ndmafv 41220 nfunsnafv 41222 afvpcfv0 41226 afvfvn0fveq 41230 afv0nbfvbi 41231 fnbrafvb 41234 afvelrn 41248 afvres 41252 tz6.12-afv 41253 dmfcoafv 41255 afvco2 41256 aovmpt4g 41281 |
Copyright terms: Public domain | W3C validator |