Definition df-f 6497

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 7046, dff3 7047, and dff4 7048. (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 6489	. 2 wff F : A --> B
5	3, 1	wfn 6488	. . 3 wff F Fn A
6	3	crn 5626	. . . 4 class ran F
7	6, 2	wss 3902	. . 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  6641  feq2  6642  feq3  6643  nff  6659  sbcfg  6661  ffn  6663  dffn2  6665  frn  6670  dffn3  6675  ffrnb  6677  fss  6679  fcof  6686  funssxp  6691  fdmrn  6694  fun  6697  fnfco  6700  fssres  6701  fcoi2  6710  fint  6714  fin  6715  f0  6716  fconst  6721  f1ssr  6737  fof  6747  dff1o2  6780  dff2  7046  dff3  7047  fmpt  7057  ffnfv  7066  ffvresb  7072  idref  7093  fpr  7101  dff1o6  7223  fliftf  7263  fiun  7889  f1iun  7890  ffoss  7892  1stcof  7965  2ndcof  7966  smores  8286  smores2  8288  iordsmo  8291  sbthlem9  9027  inf3lem6  9546  alephsmo  10016  alephsing  10190  axdc3lem2  10365  smobeth  10501  fpwwe2lem10  10555  gruiun  10714  gruima  10717  nqerf  10845  om2uzf1oi  13880  fclim  15480  invf  17696  funcres2b  17825  funcres2c  17831  hofcllem  18185  hofcl  18186  nfchnd  18538  gsumval2  18615  resmgmhm2b  18642  resmhm2b  18751  frmdss2  18792  gsumval3a  19836  subgdmdprd  19969  srgfcl  20135  lsslindf  21789  indlcim  21799  cnrest2  23234  lmss  23246  conncn  23374  txflf  23954  cnextf  24014  clsnsg  24058  tgpconncomp  24061  psmetxrge0  24261  causs  25258  ellimc2  25838  perfdvf  25864  c1lip2  25963  dvne0  25976  plyeq0  26176  plyreres  26250  aannenlem1  26296  taylf  26328  ulmss  26366  elno2  27626  elno3  27627  scutf  27790  madef  27834  onsiso  28252  mpteleeOLD  28951  ausgrusgrb  29221  ausgrumgri  29223  usgrexmplef  29315  subuhgr  29342  subupgr  29343  subumgr  29344  subusgr  29345  upgrres  29362  umgrres  29363  hhssnv  31322  pjfi  31762  maprnin  32791  cycpmconjslem1  33217  esplyfv1  33708  measdivcstALTV  34363  sitgf  34485  eulerpartlemn  34519  reprinrn  34756  cvmlift2lem9a  35478  satff  35585  icoreresf  37528  poimirlem30  37822  poimirlem31  37823  isbnd3  37956  dihf11lem  41563  ofoafg  43632  ofoaid1  43636  ofoaid2  43637  naddcnff  43640  ntrf  44400  clsf2  44403  gneispace3  44410  gneispacef2  44413  k0004lem1  44424  dvsid  44608  stoweidlem27  46307  stoweidlem29  46309  stoweidlem31  46311  fourierdlem15  46402  mbfresmf  47019  sinnpoly  47173  ffnafv  47453  fcdmvafv2v  47518  iccpartf  47713  slotresfo  49180