![]() |
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 7090, dff3 7091, and dff4 7092. (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 6529 | . 2 wff 𝐹:𝐴⟶𝐵 |
5 | 3, 1 | wfn 6528 | . . 3 wff 𝐹 Fn 𝐴 |
6 | 3 | crn 5667 | . . . 4 class ran 𝐹 |
7 | 6, 2 | wss 3940 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
8 | 5, 7 | wa 395 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
9 | 4, 8 | wb 205 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: feq1 6688 feq2 6689 feq3 6690 nff 6703 sbcfg 6705 ffn 6707 dffn2 6709 frn 6714 dffn3 6720 ffrnb 6722 fss 6724 fcof 6730 fcoOLD 6732 funssxp 6736 fdmrn 6739 fun 6743 fnfco 6746 fssres 6747 fcoi2 6756 fint 6760 fin 6761 f0 6762 fconst 6767 f1ssr 6784 fof 6795 dff1o2 6828 dff2 7090 dff3 7091 fmpt 7101 ffnfv 7110 ffvresb 7116 idref 7136 fpr 7144 dff1o6 7265 fliftf 7304 fiun 7922 f1iun 7923 ffoss 7925 1stcof 7998 2ndcof 7999 smores 8347 smores2 8349 iordsmo 8352 sbthlem9 9087 inf3lem6 9624 alephsmo 10093 alephsing 10267 axdc3lem2 10442 smobeth 10577 fpwwe2lem10 10631 gruiun 10790 gruima 10793 nqerf 10921 om2uzf1oi 13915 fclim 15494 invf 17714 funcres2b 17846 funcres2c 17853 hofcllem 18213 hofcl 18214 gsumval2 18609 resmgmhm2b 18636 resmhm2b 18737 frmdss2 18778 gsumval3a 19813 subgdmdprd 19946 srgfcl 20091 lsslindf 21693 indlcim 21703 cnrest2 23112 lmss 23124 conncn 23252 txflf 23832 cnextf 23892 clsnsg 23936 tgpconncomp 23939 psmetxrge0 24141 causs 25148 ellimc2 25728 perfdvf 25754 c1lip2 25853 dvne0 25866 plyeq0 26065 plyreres 26137 aannenlem1 26182 taylf 26214 ulmss 26250 elno2 27503 elno3 27504 scutf 27661 madef 27699 mptelee 28622 ausgrusgrb 28894 ausgrumgri 28896 usgrexmplef 28985 subuhgr 29012 subupgr 29013 subumgr 29014 subusgr 29015 upgrres 29032 umgrres 29033 hhssnv 30986 pjfi 31426 maprnin 32425 cycpmconjslem1 32781 measdivcstALTV 33712 sitgf 33835 eulerpartlemn 33869 reprinrn 34119 cvmlift2lem9a 34783 satff 34890 icoreresf 36723 poimirlem30 37008 poimirlem31 37009 isbnd3 37142 dihf11lem 40627 ofoafg 42593 ofoaid1 42597 ofoaid2 42598 naddcnff 42601 ntrf 43363 clsf2 43366 gneispace3 43373 gneispacef2 43376 k0004lem1 43387 dvsid 43579 stoweidlem27 45228 stoweidlem29 45230 stoweidlem31 45232 fourierdlem15 45323 mbfresmf 45940 ffnafv 46364 fcdmvafv2v 46429 iccpartf 46584 |
Copyright terms: Public domain | W3C validator |