![]() |
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 6682, dff3 6683, and dff4 6684. (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 6178 | . 2 wff 𝐹:𝐴⟶𝐵 |
5 | 3, 1 | wfn 6177 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5401 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 3825 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
8 | 5, 7 | wa 387 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
9 | 4, 8 | wb 198 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: feq1 6319 feq2 6320 feq3 6321 nff 6334 sbcfg 6336 ffn 6338 dffn2 6340 frn 6344 dffn3 6349 fss 6351 fco 6355 funssxp 6358 fdmrn 6361 fun 6363 fnfco 6366 fssres 6367 fcoi2 6376 fint 6381 fin 6382 f0 6383 fconst 6388 f1ssr 6404 fof 6413 dff1o2 6443 dff2 6682 dff3 6683 fmpt 6691 ffnfv 6699 ffvresb 6705 idref 6725 fpr 6733 dff1o6 6851 fliftf 6885 fun11iun 7452 ffoss 7453 1stcof 7524 2ndcof 7525 smores 7786 smores2 7788 iordsmo 7791 sbthlem9 8423 inf3lem6 8882 alephsmo 9314 alephsing 9488 axdc3lem2 9663 smobeth 9798 fpwwe2lem11 9852 gruiun 10011 gruima 10014 nqerf 10142 om2uzf1oi 13129 fclim 14761 invf 16886 funcres2b 17015 funcres2c 17019 hofcllem 17356 hofcl 17357 gsumval2 17738 resmhm2b 17819 frmdss2 17859 gsumval3a 18767 subgdmdprd 18896 srgfcl 18978 lsslindf 20666 indlcim 20676 cnrest2 21588 lmss 21600 conncn 21728 txflf 22308 cnextf 22368 clsnsg 22411 tgpconncomp 22414 psmetxrge0 22616 causs 23594 ellimc2 24168 perfdvf 24194 c1lip2 24288 dvne0 24301 plyeq0 24494 plyreres 24565 aannenlem1 24610 taylf 24642 ulmss 24678 mptelee 26374 ausgrusgrb 26643 ausgrumgri 26645 usgrexmplef 26734 subuhgr 26761 subupgr 26762 subumgr 26763 subusgr 26764 upgrres 26781 umgrres 26782 hhssnv 28810 pjfi 29252 maprnin 30208 measdivcstOLD 31085 sitgf 31207 eulerpartlemn 31241 reprinrn 31498 cvmlift2lem9a 32095 elno2 32622 elno3 32623 scutf 32734 icoreresf 34010 poimirlem30 34311 poimirlem31 34312 isbnd3 34452 dihf11lem 37795 ntrf 39781 clsf2 39784 gneispace3 39791 gneispacef2 39794 k0004lem1 39805 dvsid 40023 stoweidlem27 41689 stoweidlem29 41691 stoweidlem31 41693 fourierdlem15 41784 mbfresmf 42393 ffnafv 42722 frnvafv2v 42787 iccpartf 42909 resmgmhm2b 43375 |
Copyright terms: Public domain | W3C validator |