Definition df-f 6328

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 6842, dff3 6843, and dff4 6844. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf 6320	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6319	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5520	. . . 4 class ran 𝐹
7	6, 2	wss 3881	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 399	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6468  feq2  6469  feq3  6470  nff  6483  sbcfg  6485  ffn  6487  dffn2  6489  frn  6493  dffn3  6499  fss  6501  fco  6505  funssxp  6509  fdmrn  6512  fun  6514  fnfco  6517  fssres  6518  fcoi2  6527  fint  6532  fin  6533  f0  6534  fconst  6539  f1ssr  6556  fof  6565  dff1o2  6595  dff2  6842  dff3  6843  fmpt  6851  ffnfv  6859  ffvresb  6865  idref  6885  fpr  6893  dff1o6  7010  fliftf  7047  fiun  7626  f1iun  7627  ffoss  7629  1stcof  7701  2ndcof  7702  smores  7972  smores2  7974  iordsmo  7977  sbthlem9  8619  inf3lem6  9080  alephsmo  9513  alephsing  9687  axdc3lem2  9862  smobeth  9997  fpwwe2lem11  10051  gruiun  10210  gruima  10213  nqerf  10341  om2uzf1oi  13316  fclim  14902  invf  17030  funcres2b  17159  funcres2c  17163  hofcllem  17500  hofcl  17501  gsumval2  17888  resmhm2b  17979  frmdss2  18020  gsumval3a  19016  subgdmdprd  19149  srgfcl  19258  lsslindf  20519  indlcim  20529  cnrest2  21891  lmss  21903  conncn  22031  txflf  22611  cnextf  22671  clsnsg  22715  tgpconncomp  22718  psmetxrge0  22920  causs  23902  ellimc2  24480  perfdvf  24506  c1lip2  24601  dvne0  24614  plyeq0  24808  plyreres  24879  aannenlem1  24924  taylf  24956  ulmss  24992  mptelee  26689  ausgrusgrb  26958  ausgrumgri  26960  usgrexmplef  27049  subuhgr  27076  subupgr  27077  subumgr  27078  subusgr  27079  upgrres  27096  umgrres  27097  hhssnv  29047  pjfi  29487  maprnin  30493  cycpmconjslem1  30846  measdivcstALTV  31594  sitgf  31715  eulerpartlemn  31749  reprinrn  31999  cvmlift2lem9a  32663  satff  32770  elno2  33274  elno3  33275  scutf  33386  icoreresf  34769  poimirlem30  35087  poimirlem31  35088  isbnd3  35222  dihf11lem  38562  ntrf  40826  clsf2  40829  gneispace3  40836  gneispacef2  40839  k0004lem1  40850  dvsid  41035  stoweidlem27  42669  stoweidlem29  42671  stoweidlem31  42673  fourierdlem15  42764  mbfresmf  43373  ffnafv  43727  frnvafv2v  43792  iccpartf  43948  resmgmhm2b  44420