Definition df-f 6504

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 7053, dff3 7054, and dff4 7055. (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 6496	. 2 wff F : A --> B
5	3, 1	wfn 6495	. . 3 wff F Fn A
6	3	crn 5633	. . . 4 class ran F
7	6, 2	wss 3903	. . 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  6648  feq2  6649  feq3  6650  nff  6666  sbcfg  6668  ffn  6670  dffn2  6672  frn  6677  dffn3  6682  ffrnb  6684  fss  6686  fcof  6693  funssxp  6698  fdmrn  6701  fun  6704  fnfco  6707  fssres  6708  fcoi2  6717  fint  6721  fin  6722  f0  6723  fconst  6728  f1ssr  6744  fof  6754  dff1o2  6787  dff2  7053  dff3  7054  fmpt  7064  ffnfv  7073  ffvresb  7080  idref  7101  fpr  7109  dff1o6  7231  fliftf  7271  fiun  7897  f1iun  7898  ffoss  7900  1stcof  7973  2ndcof  7974  smores  8294  smores2  8296  iordsmo  8299  sbthlem9  9035  inf3lem6  9554  alephsmo  10024  alephsing  10198  axdc3lem2  10373  smobeth  10509  fpwwe2lem10  10563  gruiun  10722  gruima  10725  nqerf  10853  om2uzf1oi  13888  fclim  15488  invf  17704  funcres2b  17833  funcres2c  17839  hofcllem  18193  hofcl  18194  nfchnd  18546  gsumval2  18623  resmgmhm2b  18650  resmhm2b  18759  frmdss2  18800  gsumval3a  19844  subgdmdprd  19977  srgfcl  20143  lsslindf  21797  indlcim  21807  cnrest2  23242  lmss  23254  conncn  23382  txflf  23962  cnextf  24022  clsnsg  24066  tgpconncomp  24069  psmetxrge0  24269  causs  25266  ellimc2  25846  perfdvf  25872  c1lip2  25971  dvne0  25984  plyeq0  26184  plyreres  26258  aannenlem1  26304  taylf  26336  ulmss  26374  elno2  27634  elno3  27635  cutsf  27800  madef  27844  oniso  28279  mpteleeOLD  28980  ausgrusgrb  29250  ausgrumgri  29252  usgrexmplef  29344  subuhgr  29371  subupgr  29372  subumgr  29373  subusgr  29374  upgrres  29391  umgrres  29392  hhssnv  31352  pjfi  31792  maprnin  32821  cycpmconjslem1  33248  esplyfv1  33746  measdivcstALTV  34403  sitgf  34525  eulerpartlemn  34559  reprinrn  34796  cvmlift2lem9a  35519  satff  35626  icoreresf  37607  poimirlem30  37901  poimirlem31  37902  isbnd3  38035  dihf11lem  41642  ofoafg  43711  ofoaid1  43715  ofoaid2  43716  naddcnff  43719  ntrf  44479  clsf2  44482  gneispace3  44489  gneispacef2  44492  k0004lem1  44503  dvsid  44687  stoweidlem27  46385  stoweidlem29  46387  stoweidlem31  46389  fourierdlem15  46480  mbfresmf  47097  sinnpoly  47251  ffnafv  47531  fcdmvafv2v  47596  iccpartf  47791  slotresfo  49258