Definition df-f 6491

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. F : A --> B can be read as " F is a function from A to B". For alternate definitions, see dff2 7038, dff3 7039, and dff4 7040. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf 6483	. 2 wff F : A --> B
5	3, 1	wfn 6482	. . 3 wff F Fn A
6	3	crn 5620	. . . 4 class ran F
7	6, 2	wss 3897	. . 3 wff ran F C_ B
8	5, 7	wa 395	. 2 wff ( F Fn A /\ ran F C_ B )
9	4, 8	wb 206	1 wff ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )

This definition is referenced by:  feq1  6635  feq2  6636  feq3  6637  nff  6653  sbcfg  6655  ffn  6657  dffn2  6659  frn  6664  dffn3  6669  ffrnb  6671  fss  6673  fcof  6680  funssxp  6685  fdmrn  6688  fun  6691  fnfco  6694  fssres  6695  fcoi2  6704  fint  6708  fin  6709  f0  6710  fconst  6715  f1ssr  6731  fof  6741  dff1o2  6774  dff2  7038  dff3  7039  fmpt  7049  ffnfv  7058  ffvresb  7064  idref  7085  fpr  7093  dff1o6  7215  fliftf  7255  fiun  7881  f1iun  7882  ffoss  7884  1stcof  7957  2ndcof  7958  smores  8278  smores2  8280  iordsmo  8283  sbthlem9  9014  inf3lem6  9529  alephsmo  9999  alephsing  10173  axdc3lem2  10348  smobeth  10483  fpwwe2lem10  10537  gruiun  10696  gruima  10699  nqerf  10827  om2uzf1oi  13866  fclim  15466  invf  17681  funcres2b  17810  funcres2c  17816  hofcllem  18170  hofcl  18171  nfchnd  18523  gsumval2  18600  resmgmhm2b  18627  resmhm2b  18736  frmdss2  18777  gsumval3a  19821  subgdmdprd  19954  srgfcl  20120  lsslindf  21773  indlcim  21783  cnrest2  23207  lmss  23219  conncn  23347  txflf  23927  cnextf  23987  clsnsg  24031  tgpconncomp  24034  psmetxrge0  24234  causs  25231  ellimc2  25811  perfdvf  25837  c1lip2  25936  dvne0  25949  plyeq0  26149  plyreres  26223  aannenlem1  26269  taylf  26301  ulmss  26339  elno2  27599  elno3  27600  scutf  27759  madef  27803  onsiso  28211  mpteleeOLD  28880  ausgrusgrb  29150  ausgrumgri  29152  usgrexmplef  29244  subuhgr  29271  subupgr  29272  subumgr  29273  subusgr  29274  upgrres  29291  umgrres  29292  hhssnv  31251  pjfi  31691  maprnin  32721  cycpmconjslem1  33130  esplyfv1  33597  measdivcstALTV  34245  sitgf  34367  eulerpartlemn  34401  reprinrn  34638  cvmlift2lem9a  35354  satff  35461  icoreresf  37403  poimirlem30  37696  poimirlem31  37697  isbnd3  37830  dihf11lem  41371  ofoafg  43452  ofoaid1  43456  ofoaid2  43457  naddcnff  43460  ntrf  44221  clsf2  44224  gneispace3  44231  gneispacef2  44234  k0004lem1  44245  dvsid  44429  stoweidlem27  46130  stoweidlem29  46132  stoweidlem31  46134  fourierdlem15  46225  mbfresmf  46842  sinnpoly  46996  ffnafv  47276  fcdmvafv2v  47341  iccpartf  47536  slotresfo  49004