| 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 7119, dff3 7120, and dff4 7121. (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 6557 | . 2 wff 𝐹:𝐴⟶𝐵 |
| 5 | 3, 1 | wfn 6556 | . . 3 wff 𝐹 Fn 𝐴 |
| 6 | 3 | crn 5686 | . . . 4 class ran 𝐹 |
| 7 | 6, 2 | wss 3951 | . . 3 wff ran 𝐹 ⊆ 𝐵 |
| 8 | 5, 7 | wa 395 | . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) |
| 9 | 4, 8 | wb 206 | 1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: feq1 6716 feq2 6717 feq3 6718 nff 6732 sbcfg 6734 ffn 6736 dffn2 6738 frn 6743 dffn3 6748 ffrnb 6750 fss 6752 fcof 6759 funssxp 6764 fdmrn 6767 fun 6770 fnfco 6773 fssres 6774 fcoi2 6783 fint 6787 fin 6788 f0 6789 fconst 6794 f1ssr 6810 fof 6820 dff1o2 6853 dff2 7119 dff3 7120 fmpt 7130 ffnfv 7139 ffvresb 7145 idref 7166 fpr 7174 dff1o6 7295 fliftf 7335 fiun 7967 f1iun 7968 ffoss 7970 1stcof 8044 2ndcof 8045 smores 8392 smores2 8394 iordsmo 8397 sbthlem9 9131 inf3lem6 9673 alephsmo 10142 alephsing 10316 axdc3lem2 10491 smobeth 10626 fpwwe2lem10 10680 gruiun 10839 gruima 10842 nqerf 10970 om2uzf1oi 13994 fclim 15589 invf 17812 funcres2b 17942 funcres2c 17948 hofcllem 18303 hofcl 18304 gsumval2 18699 resmgmhm2b 18726 resmhm2b 18835 frmdss2 18876 gsumval3a 19921 subgdmdprd 20054 srgfcl 20193 lsslindf 21850 indlcim 21860 cnrest2 23294 lmss 23306 conncn 23434 txflf 24014 cnextf 24074 clsnsg 24118 tgpconncomp 24121 psmetxrge0 24323 causs 25332 ellimc2 25912 perfdvf 25938 c1lip2 26037 dvne0 26050 plyeq0 26250 plyreres 26324 aannenlem1 26370 taylf 26402 ulmss 26440 elno2 27699 elno3 27700 scutf 27857 madef 27895 mptelee 28910 ausgrusgrb 29182 ausgrumgri 29184 usgrexmplef 29276 subuhgr 29303 subupgr 29304 subumgr 29305 subusgr 29306 upgrres 29323 umgrres 29324 hhssnv 31283 pjfi 31723 maprnin 32742 cycpmconjslem1 33174 measdivcstALTV 34226 sitgf 34349 eulerpartlemn 34383 reprinrn 34633 cvmlift2lem9a 35308 satff 35415 icoreresf 37353 poimirlem30 37657 poimirlem31 37658 isbnd3 37791 dihf11lem 41268 ofoafg 43367 ofoaid1 43371 ofoaid2 43372 naddcnff 43375 ntrf 44136 clsf2 44139 gneispace3 44146 gneispacef2 44149 k0004lem1 44160 dvsid 44350 stoweidlem27 46042 stoweidlem29 46044 stoweidlem31 46046 fourierdlem15 46137 mbfresmf 46754 ffnafv 47183 fcdmvafv2v 47248 iccpartf 47418 |
| Copyright terms: Public domain | W3C validator |