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

Definition df-f 6101
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 6589, dff3 6590, and dff4 6591. (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 6093 . 2 wff 𝐹:𝐴𝐵
53, 1wfn 6092 . . 3 wff 𝐹 Fn 𝐴
63crn 5312 . . . 4 class ran 𝐹
76, 2wss 3769 . . 3 wff ran 𝐹𝐵
85, 7wa 384 . 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵)
94, 8wb 197 1 wff (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  feq1  6233  feq2  6234  feq3  6235  nff  6248  sbcfg  6250  ffn  6252  dffn2  6254  frn  6258  dffn3  6263  fss  6265  fco  6269  funssxp  6272  fdmrn  6275  fun  6277  fnfco  6280  fssres  6281  fcoi2  6290  fint  6295  fin  6296  f0  6297  fconst  6302  f1ssr  6318  fof  6327  dff1o2  6354  dff2  6589  dff3  6590  fmpt  6598  ffnfv  6606  ffvresb  6612  idref  6631  fpr  6641  dff1o6  6751  fliftf  6785  fun11iun  7352  ffoss  7353  1stcof  7424  2ndcof  7425  smores  7681  smores2  7683  iordsmo  7686  sbthlem9  8313  sucdom2  8391  inf3lem6  8773  alephsmo  9204  alephsing  9379  axdc3lem2  9554  smobeth  9689  fpwwe2lem11  9743  gch3  9779  gruiun  9902  gruima  9905  nqerf  10033  om2uzf1oi  12972  fclim  14503  invf  16628  funcres2b  16757  funcres2c  16761  hofcllem  17099  hofcl  17100  gsumval2  17481  resmhm2b  17562  frmdss2  17601  gsumval3a  18501  subgdmdprd  18631  srgfcl  18713  lsslindf  20375  indlcim  20385  cnrest2  21300  lmss  21312  conncn  21439  txflf  22019  cnextf  22079  clsnsg  22122  tgpconncomp  22125  psmetxrge0  22327  causs  23304  ellimc2  23851  perfdvf  23877  c1lip2  23971  dvne0  23984  plyeq0  24177  plyreres  24248  aannenlem1  24293  taylf  24325  ulmss  24361  mptelee  25985  ausgrusgrb  26271  ausgrumgri  26273  usgrexmplef  26363  subuhgr  26390  subupgr  26391  subumgr  26392  subusgr  26393  upgrres  26410  umgrres  26411  hhssnv  28445  pjfi  28887  maprnin  29829  measdivcstOLD  30608  sitgf  30730  eulerpartlemn  30764  reprinrn  31017  cvmlift2lem9a  31603  elno2  32123  elno3  32124  scutf  32235  icoreresf  33511  poimirlem30  33747  poimirlem31  33748  isbnd3  33889  dihf11lem  37041  ntrf  38915  clsf2  38918  gneispace3  38925  gneispacef2  38928  gneispacern  38930  k0004lem1  38939  dvsid  39024  stoweidlem27  40717  stoweidlem29  40719  stoweidlem31  40721  fourierdlem15  40812  mbfresmf  41424  ffnafv  41754  frnvafv2v  41819  iccpartf  41936  resmgmhm2b  42362
  Copyright terms: Public domain W3C validator