Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-f | Unicode version |
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cF | . . 3 | |
4 | 1, 2, 3 | wf 5089 | . 2 |
5 | 3, 1 | wfn 5088 | . . 3 |
6 | 3 | crn 4510 | . . . 4 |
7 | 6, 2 | wss 3041 | . . 3 |
8 | 5, 7 | wa 103 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: feq1 5225 feq2 5226 feq3 5227 nff 5239 sbcfg 5241 ffn 5242 dffn2 5244 frn 5251 dffn3 5253 fss 5254 fco 5258 funssxp 5262 fun 5265 fnfco 5267 fssres 5268 fcoi2 5274 fintm 5278 fin 5279 f0 5283 fconst 5288 f1ssr 5305 fof 5315 dff1o2 5340 fun11iun 5356 ffoss 5367 dff2 5532 fmpt 5538 ffnfv 5546 ffvresb 5551 fpr 5570 fprg 5571 idref 5626 dff1o6 5645 fliftf 5668 1stcof 6029 2ndcof 6030 smores 6157 smores2 6159 iordsmo 6162 tfrcllembfn 6222 sbthlemi9 6821 inresflem 6913 frec2uzf1od 10134 frecuzrdgtcl 10140 fclim 11018 ennnfonelemf1 11842 cnrest2 12316 lmss 12326 psmetxrge0 12412 dvfgg 12737 nninfall 13100 |
Copyright terms: Public domain | W3C validator |