![]() |
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 6411, dff3 6412, and dff4 6413. (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 5922 | . 2 wff 𝐹:𝐴⟶𝐵 |
5 | 3, 1 | wfn 5921 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5144 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 3607 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
8 | 5, 7 | wa 383 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
9 | 4, 8 | wb 196 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: feq1 6064 feq2 6065 feq3 6066 nff 6079 sbcfg 6081 ffn 6083 dffn2 6085 frn 6091 dffn3 6092 fss 6094 fco 6096 funssxp 6099 fdmrn 6102 fun 6104 fnfco 6107 fssres 6108 fcoi2 6117 fint 6122 fin 6123 f0 6124 fconst 6129 f1ssr 6145 fof 6153 dff1o2 6180 dff2 6411 dff3 6412 fmpt 6421 ffnfv 6428 ffvresb 6434 fpr 6461 idref 6539 dff1o6 6571 fliftf 6605 fun11iun 7168 ffoss 7169 1stcof 7240 2ndcof 7241 smores 7494 smores2 7496 iordsmo 7499 sbthlem9 8119 sucdom2 8197 inf3lem6 8568 alephsmo 8963 alephsing 9136 axdc3lem2 9311 smobeth 9446 fpwwe2lem11 9500 gch3 9536 gruiun 9659 gruima 9662 nqerf 9790 om2uzf1oi 12792 fclim 14328 invf 16475 funcres2b 16604 funcres2c 16608 hofcllem 16945 hofcl 16946 gsumval2 17327 resmhm2b 17408 frmdss2 17447 gsumval3a 18350 subgdmdprd 18479 srgfcl 18561 lsslindf 20217 indlcim 20227 cnrest2 21138 lmss 21150 conncn 21277 txflf 21857 cnextf 21917 clsnsg 21960 tgpconncomp 21963 psmetxrge0 22165 causs 23142 ellimc2 23686 perfdvf 23712 c1lip2 23806 dvne0 23819 plyeq0 24012 plyreres 24083 aannenlem1 24128 taylf 24160 ulmss 24196 mptelee 25820 ausgrusgrb 26105 ausgrumgri 26107 usgrexmplef 26196 subuhgr 26223 subupgr 26224 subumgr 26225 subusgr 26226 upgrres 26243 umgrres 26244 hhssnv 28249 pjfi 28691 maprnin 29634 measdivcstOLD 30415 sitgf 30537 eulerpartlemn 30571 reprinrn 30824 cvmlift2lem9a 31411 elno2 31932 elno3 31933 scutf 32044 icoreresf 33330 poimirlem30 33569 poimirlem31 33570 isbnd3 33713 dihf11lem 36872 ntrf 38738 clsf2 38741 gneispace3 38748 gneispacef2 38751 gneispacern 38753 k0004lem1 38762 dvsid 38847 stoweidlem27 40562 stoweidlem29 40564 stoweidlem31 40566 fourierdlem15 40657 mbfresmf 41269 ffnafv 41572 iccpartf 41692 resmgmhm2b 42125 |
Copyright terms: Public domain | W3C validator |