![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > df-f | Unicode version |
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5419, dff3 5420, and dff4 5421. (Contributed by SF, 5-Jan-2015.) |
Ref | Expression |
---|---|
df-f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cF |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | wf 4777 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 3, 1 | wfn 4776 |
. . 3
![]() ![]() ![]() ![]() |
6 | 3 | crn 4773 |
. . . 4
![]() ![]() ![]() |
7 | 6, 2 | wss 3257 |
. . 3
![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | wa 358 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 176 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: feq1 5210 feq2 5211 feq3 5212 nff 5221 ffn 5223 dffn2 5224 frn 5228 dffn3 5229 fss 5230 fco 5231 funssxp 5233 fun 5236 fnfco 5237 fssres 5238 fint 5245 fin 5246 f0 5248 fconst 5250 f1funfun 5263 fof 5269 dff1o2 5291 fun11iun 5305 ffoss 5314 dff2 5419 dff3 5420 ffnfv 5427 ffvresb 5431 fpr 5437 dff1o6 5475 fmpt 5692 fmpt2d 5695 mapexi 6003 map0e 6023 ovcelem1 6171 ceex 6174 fce 6188 sbthlem1 6203 |
Copyright terms: Public domain | W3C validator |