Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-f | Structured version Visualization version Unicode version |
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. can be read as " is a function from to ". For alternate definitions, see dff2 6371, dff3 6372, and dff4 6373. (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 5884 | . 2 |
5 | 3, 1 | wfn 5883 | . . 3 |
6 | 3 | crn 5115 | . . . 4 |
7 | 6, 2 | wss 3574 | . . 3 |
8 | 5, 7 | wa 384 | . 2 |
9 | 4, 8 | wb 196 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: feq1 6026 feq2 6027 feq3 6028 nff 6041 sbcfg 6043 ffn 6045 dffn2 6047 frn 6053 dffn3 6054 fss 6056 fco 6058 funssxp 6061 fdmrn 6064 fun 6066 fnfco 6069 fssres 6070 fcoi2 6079 fint 6084 fin 6085 f0 6086 fconst 6091 f1ssr 6107 fof 6115 dff1o2 6142 dff2 6371 dff3 6372 fmpt 6381 ffnfv 6388 ffvresb 6394 fpr 6421 idref 6499 dff1o6 6531 fliftf 6565 fun11iun 7126 ffoss 7127 1stcof 7196 2ndcof 7197 smores 7449 smores2 7451 iordsmo 7454 sbthlem9 8078 sucdom2 8156 inf3lem6 8530 alephsmo 8925 alephsing 9098 axdc3lem2 9273 smobeth 9408 fpwwe2lem11 9462 gch3 9498 gruiun 9621 gruima 9624 nqerf 9752 om2uzf1oi 12752 fclim 14284 invf 16428 funcres2b 16557 funcres2c 16561 hofcllem 16898 hofcl 16899 gsumval2 17280 resmhm2b 17361 frmdss2 17400 gsumval3a 18304 subgdmdprd 18433 srgfcl 18515 lsslindf 20169 indlcim 20179 cnrest2 21090 lmss 21102 conncn 21229 txflf 21810 cnextf 21870 clsnsg 21913 tgpconncomp 21916 psmetxrge0 22118 causs 23096 ellimc2 23641 perfdvf 23667 c1lip2 23761 dvne0 23774 plyeq0 23967 plyreres 24038 aannenlem1 24083 taylf 24115 ulmss 24151 mptelee 25775 ausgrusgrb 26060 ausgrumgri 26062 usgrexmplef 26151 subuhgr 26178 subupgr 26179 subumgr 26180 subusgr 26181 upgrres 26198 umgrres 26199 hhssnv 28121 pjfi 28563 maprnin 29506 measdivcstOLD 30287 sitgf 30409 eulerpartlemn 30443 reprinrn 30696 cvmlift2lem9a 31285 elno2 31807 elno3 31808 scutf 31919 icoreresf 33200 poimirlem30 33439 poimirlem31 33440 isbnd3 33583 dihf11lem 36555 ntrf 38421 clsf2 38424 gneispace3 38431 gneispacef2 38434 gneispacern 38436 k0004lem1 38445 dvsid 38530 stoweidlem27 40244 stoweidlem29 40246 stoweidlem31 40248 fourierdlem15 40339 mbfresmf 40948 ffnafv 41251 iccpartf 41367 resmgmhm2b 41800 |
Copyright terms: Public domain | W3C validator |