Definition df-f 6486

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 7033, dff3 7034, and dff4 7035. (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 6478	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6477	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5620	. . . 4 class ran 𝐹
7	6, 2	wss 3903	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 206	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6630  feq2  6631  feq3  6632  nff  6648  sbcfg  6650  ffn  6652  dffn2  6654  frn  6659  dffn3  6664  ffrnb  6666  fss  6668  fcof  6675  funssxp  6680  fdmrn  6683  fun  6686  fnfco  6689  fssres  6690  fcoi2  6699  fint  6703  fin  6704  f0  6705  fconst  6710  f1ssr  6726  fof  6736  dff1o2  6769  dff2  7033  dff3  7034  fmpt  7044  ffnfv  7053  ffvresb  7059  idref  7080  fpr  7088  dff1o6  7212  fliftf  7252  fiun  7878  f1iun  7879  ffoss  7881  1stcof  7954  2ndcof  7955  smores  8275  smores2  8277  iordsmo  8280  sbthlem9  9012  inf3lem6  9529  alephsmo  9996  alephsing  10170  axdc3lem2  10345  smobeth  10480  fpwwe2lem10  10534  gruiun  10693  gruima  10696  nqerf  10824  om2uzf1oi  13860  fclim  15460  invf  17675  funcres2b  17804  funcres2c  17810  hofcllem  18164  hofcl  18165  gsumval2  18560  resmgmhm2b  18587  resmhm2b  18696  frmdss2  18737  gsumval3a  19782  subgdmdprd  19915  srgfcl  20081  lsslindf  21737  indlcim  21747  cnrest2  23171  lmss  23183  conncn  23311  txflf  23891  cnextf  23951  clsnsg  23995  tgpconncomp  23998  psmetxrge0  24199  causs  25196  ellimc2  25776  perfdvf  25802  c1lip2  25901  dvne0  25914  plyeq0  26114  plyreres  26188  aannenlem1  26234  taylf  26266  ulmss  26304  elno2  27564  elno3  27565  scutf  27723  madef  27766  onsiso  28174  mptelee  28840  ausgrusgrb  29110  ausgrumgri  29112  usgrexmplef  29204  subuhgr  29231  subupgr  29232  subumgr  29233  subusgr  29234  upgrres  29251  umgrres  29252  hhssnv  31208  pjfi  31648  maprnin  32674  cycpmconjslem1  33096  measdivcstALTV  34192  sitgf  34315  eulerpartlemn  34349  reprinrn  34586  cvmlift2lem9a  35280  satff  35387  icoreresf  37330  poimirlem30  37634  poimirlem31  37635  isbnd3  37768  dihf11lem  41249  ofoafg  43331  ofoaid1  43335  ofoaid2  43336  naddcnff  43339  ntrf  44100  clsf2  44103  gneispace3  44110  gneispacef2  44113  k0004lem1  44124  dvsid  44308  stoweidlem27  46012  stoweidlem29  46014  stoweidlem31  46016  fourierdlem15  46107  mbfresmf  46724  sinnpoly  46879  ffnafv  47159  fcdmvafv2v  47224  iccpartf  47419  slotresfo  48887