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 6858, dff3 6859, and dff4 6860. (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 6345 | . 2 wff 𝐹:𝐴⟶𝐵 |
5 | 3, 1 | wfn 6344 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5550 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 3935 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
8 | 5, 7 | wa 396 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
9 | 4, 8 | wb 207 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: feq1 6489 feq2 6490 feq3 6491 nff 6504 sbcfg 6506 ffn 6508 dffn2 6510 frn 6514 dffn3 6519 fss 6521 fco 6525 funssxp 6529 fdmrn 6532 fun 6534 fnfco 6537 fssres 6538 fcoi2 6547 fint 6552 fin 6553 f0 6554 fconst 6559 f1ssr 6575 fof 6584 dff1o2 6614 dff2 6858 dff3 6859 fmpt 6867 ffnfv 6875 ffvresb 6881 idref 6901 fpr 6909 dff1o6 7023 fliftf 7057 fiunw 7632 f1iunw 7633 fiun 7635 f1iun 7636 ffoss 7638 1stcof 7710 2ndcof 7711 smores 7980 smores2 7982 iordsmo 7985 sbthlem9 8624 inf3lem6 9085 alephsmo 9517 alephsing 9687 axdc3lem2 9862 smobeth 9997 fpwwe2lem11 10051 gruiun 10210 gruima 10213 nqerf 10341 om2uzf1oi 13311 fclim 14900 invf 17028 funcres2b 17157 funcres2c 17161 hofcllem 17498 hofcl 17499 gsumval2 17886 resmhm2b 17977 frmdss2 18018 gsumval3a 18954 subgdmdprd 19087 srgfcl 19196 lsslindf 20904 indlcim 20914 cnrest2 21824 lmss 21836 conncn 21964 txflf 22544 cnextf 22604 clsnsg 22647 tgpconncomp 22650 psmetxrge0 22852 causs 23830 ellimc2 24404 perfdvf 24430 c1lip2 24524 dvne0 24537 plyeq0 24730 plyreres 24801 aannenlem1 24846 taylf 24878 ulmss 24914 mptelee 26609 ausgrusgrb 26878 ausgrumgri 26880 usgrexmplef 26969 subuhgr 26996 subupgr 26997 subumgr 26998 subusgr 26999 upgrres 27016 umgrres 27017 hhssnv 28969 pjfi 29409 maprnin 30394 cycpmconjslem1 30724 measdivcstALTV 31384 sitgf 31505 eulerpartlemn 31539 reprinrn 31789 cvmlift2lem9a 32448 satff 32555 elno2 33059 elno3 33060 scutf 33171 icoreresf 34516 poimirlem30 34804 poimirlem31 34805 isbnd3 34945 dihf11lem 38284 ntrf 40353 clsf2 40356 gneispace3 40363 gneispacef2 40366 k0004lem1 40377 dvsid 40543 stoweidlem27 42193 stoweidlem29 42195 stoweidlem31 42197 fourierdlem15 42288 mbfresmf 42897 ffnafv 43251 frnvafv2v 43316 iccpartf 43438 resmgmhm2b 43914 |
Copyright terms: Public domain | W3C validator |