Definition df-f 6537

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 7090, dff3 7091, and dff4 7092. (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 6529	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6528	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5667	. . . 4 class ran 𝐹
7	6, 2	wss 3940	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 205	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6688  feq2  6689  feq3  6690  nff  6703  sbcfg  6705  ffn  6707  dffn2  6709  frn  6714  dffn3  6720  ffrnb  6722  fss  6724  fcof  6730  fcoOLD  6732  funssxp  6736  fdmrn  6739  fun  6743  fnfco  6746  fssres  6747  fcoi2  6756  fint  6760  fin  6761  f0  6762  fconst  6767  f1ssr  6784  fof  6795  dff1o2  6828  dff2  7090  dff3  7091  fmpt  7101  ffnfv  7110  ffvresb  7116  idref  7136  fpr  7144  dff1o6  7265  fliftf  7304  fiun  7922  f1iun  7923  ffoss  7925  1stcof  7998  2ndcof  7999  smores  8347  smores2  8349  iordsmo  8352  sbthlem9  9087  inf3lem6  9624  alephsmo  10093  alephsing  10267  axdc3lem2  10442  smobeth  10577  fpwwe2lem10  10631  gruiun  10790  gruima  10793  nqerf  10921  om2uzf1oi  13915  fclim  15494  invf  17714  funcres2b  17846  funcres2c  17853  hofcllem  18213  hofcl  18214  gsumval2  18609  resmgmhm2b  18636  resmhm2b  18737  frmdss2  18778  gsumval3a  19813  subgdmdprd  19946  srgfcl  20091  lsslindf  21693  indlcim  21703  cnrest2  23112  lmss  23124  conncn  23252  txflf  23832  cnextf  23892  clsnsg  23936  tgpconncomp  23939  psmetxrge0  24141  causs  25148  ellimc2  25728  perfdvf  25754  c1lip2  25853  dvne0  25866  plyeq0  26065  plyreres  26137  aannenlem1  26182  taylf  26214  ulmss  26250  elno2  27503  elno3  27504  scutf  27661  madef  27699  mptelee  28622  ausgrusgrb  28894  ausgrumgri  28896  usgrexmplef  28985  subuhgr  29012  subupgr  29013  subumgr  29014  subusgr  29015  upgrres  29032  umgrres  29033  hhssnv  30986  pjfi  31426  maprnin  32425  cycpmconjslem1  32781  measdivcstALTV  33712  sitgf  33835  eulerpartlemn  33869  reprinrn  34119  cvmlift2lem9a  34783  satff  34890  icoreresf  36723  poimirlem30  37008  poimirlem31  37009  isbnd3  37142  dihf11lem  40627  ofoafg  42593  ofoaid1  42597  ofoaid2  42598  naddcnff  42601  ntrf  43363  clsf2  43366  gneispace3  43373  gneispacef2  43376  k0004lem1  43387  dvsid  43579  stoweidlem27  45228  stoweidlem29  45230  stoweidlem31  45232  fourierdlem15  45323  mbfresmf  45940  ffnafv  46364  fcdmvafv2v  46429  iccpartf  46584