Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-f | Structured version Visualization version GIF 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 6279, dff3 6280, and dff4 6281. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
df-f | ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | cF | . . 3 class 𝐹 | |
4 | 1, 2, 3 | wf 5800 | . 2 wff 𝐹:𝐴⟶𝐵 |
5 | 3, 1 | wfn 5799 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5039 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 3540 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
8 | 5, 7 | wa 383 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
9 | 4, 8 | wb 195 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: feq1 5939 feq2 5940 feq3 5941 nff 5954 sbcfg 5956 ffn 5958 dffn2 5960 frn 5966 dffn3 5967 fss 5969 fco 5971 funssxp 5974 fdmrn 5977 fun 5979 fnfco 5982 fssres 5983 fcoi2 5992 fint 5997 fin 5998 f0 5999 fconst 6004 f1ssr 6020 fof 6028 dff1o2 6055 dff2 6279 dff3 6280 fmpt 6289 ffnfv 6295 ffvresb 6301 fpr 6326 idref 6403 dff1o6 6431 fliftf 6465 fun11iun 7019 ffoss 7020 1stcof 7087 2ndcof 7088 smores 7336 smores2 7338 iordsmo 7341 sbthlem9 7963 sucdom2 8041 inf3lem6 8413 alephsmo 8808 alephsing 8981 axdc3lem2 9156 smobeth 9287 fpwwe2lem11 9341 gch3 9377 gruiun 9500 gruima 9503 nqerf 9631 om2uzf1oi 12614 fclim 14132 invf 16251 funcres2b 16380 funcres2c 16384 hofcllem 16721 hofcl 16722 gsumval2 17103 resmhm2b 17184 frmdss2 17223 gsumval3a 18127 subgdmdprd 18256 srgfcl 18338 lsslindf 19988 indlcim 19998 cnrest2 20900 lmss 20912 concn 21039 txflf 21620 cnextf 21680 clsnsg 21723 tgpconcomp 21726 psmetxrge0 21928 causs 22904 ellimc2 23447 perfdvf 23473 c1lip2 23565 dvne0 23578 plyeq0 23771 plyreres 23842 aannenlem1 23887 taylf 23919 ulmss 23955 mptelee 25575 ausisusgra 25884 usgraedgrnv 25906 usgraexmplef 25929 cusgrarn 25988 hhssnv 27505 pjfi 27947 maprnin 28894 measdivcstOLD 29614 sitgf 29736 eulerpartlemn 29770 cvmlift2lem9a 30539 elno2 31051 elno3 31052 nodenselem6 31085 icoreresf 32376 poimirlem30 32609 poimirlem31 32610 isbnd3 32753 dihf11lem 35573 ntrf 37441 clsf2 37444 gneispace3 37451 gneispacef2 37454 gneispacern 37456 k0004lem1 37465 dvsid 37552 stoweidlem27 38920 stoweidlem29 38922 stoweidlem31 38924 fourierdlem15 39015 mbfresmf 39626 ffnafv 39900 iccpartf 39969 ausgrusgrb 40395 ausgrumgri 40397 subuhgr 40510 subupgr 40511 subumgr 40512 subusgr 40513 resmgmhm2b 41590 |
Copyright terms: Public domain | W3C validator |