Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f Structured version   Visualization version   GIF version

Definition df-f 5808
 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 6279, dff3 6280, and dff4 6281. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf 5800 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 5799 . . 3 wff 𝐹 Fn 𝐴
63crn 5039 . . . 4 class ran 𝐹
76, 2wss 3540 . . 3 wff ran 𝐹𝐵
85, 7wa 383 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 195 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
 Colors of variables: wff setvar class This definition is referenced by:  feq1  5939  feq2  5940  feq3  5941  nff  5954  sbcfg  5956  ffn  5958  dffn2  5960  frn  5966  dffn3  5967  fss  5969  fco  5971  funssxp  5974  fdmrn  5977  fun  5979  fnfco  5982  fssres  5983  fcoi2  5992  fint  5997  fin  5998  f0  5999  fconst  6004  f1ssr  6020  fof  6028  dff1o2  6055  dff2  6279  dff3  6280  fmpt  6289  ffnfv  6295  ffvresb  6301  fpr  6326  idref  6403  dff1o6  6431  fliftf  6465  fun11iun  7019  ffoss  7020  1stcof  7087  2ndcof  7088  smores  7336  smores2  7338  iordsmo  7341  sbthlem9  7963  sucdom2  8041  inf3lem6  8413  alephsmo  8808  alephsing  8981  axdc3lem2  9156  smobeth  9287  fpwwe2lem11  9341  gch3  9377  gruiun  9500  gruima  9503  nqerf  9631  om2uzf1oi  12614  fclim  14132  invf  16251  funcres2b  16380  funcres2c  16384  hofcllem  16721  hofcl  16722  gsumval2  17103  resmhm2b  17184  frmdss2  17223  gsumval3a  18127  subgdmdprd  18256  srgfcl  18338  lsslindf  19988  indlcim  19998  cnrest2  20900  lmss  20912  concn  21039  txflf  21620  cnextf  21680  clsnsg  21723  tgpconcomp  21726  psmetxrge0  21928  causs  22904  ellimc2  23447  perfdvf  23473  c1lip2  23565  dvne0  23578  plyeq0  23771  plyreres  23842  aannenlem1  23887  taylf  23919  ulmss  23955  mptelee  25575  ausisusgra  25884  usgraedgrnv  25906  usgraexmplef  25929  cusgrarn  25988  hhssnv  27505  pjfi  27947  maprnin  28894  measdivcstOLD  29614  sitgf  29736  eulerpartlemn  29770  cvmlift2lem9a  30539  elno2  31051  elno3  31052  nodenselem6  31085  icoreresf  32376  poimirlem30  32609  poimirlem31  32610  isbnd3  32753  dihf11lem  35573  ntrf  37441  clsf2  37444  gneispace3  37451  gneispacef2  37454  gneispacern  37456  k0004lem1  37465  dvsid  37552  stoweidlem27  38920  stoweidlem29  38922  stoweidlem31  38924  fourierdlem15  39015  mbfresmf  39626  ffnafv  39900  iccpartf  39969  ausgrusgrb  40395  ausgrumgri  40397  subuhgr  40510  subupgr  40511  subumgr  40512  subusgr  40513  resmgmhm2b  41590
 Copyright terms: Public domain W3C validator