Definition df-f 6492

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 7043, dff3 7044, and dff4 7045. (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 6484	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6483	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5621	. . . 4 class ran 𝐹
7	6, 2	wss 3884	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 397	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 208	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6636  feq2  6637  feq3  6638  nff  6654  sbcfg  6656  ffn  6658  dffn2  6660  frn  6665  dffn3  6670  ffrnb  6672  fss  6674  fcof  6681  funssxp  6686  fdmrn  6689  fun  6692  fnfco  6695  fssres  6696  fcoi2  6705  fint  6709  fin  6710  f0  6711  fconst  6716  f1ssr  6732  fof  6742  dff1o2  6775  dff2  7043  dff3  7044  fmpt  7054  ffnfv  7063  ffvresb  7070  idref  7091  fpr  7100  dff1o6  7222  fliftf  7262  fiun  7887  f1iun  7888  ffoss  7890  1stcof  7963  2ndcof  7964  smores  8285  smores2  8287  iordsmo  8290  sbthlem9  9027  inf3lem6  9549  alephsmo  10019  alephsing  10194  axdc3lem2  10369  smobeth  10505  fpwwe2lem10  10559  gruiun  10718  gruima  10721  nqerf  10849  om2uzf1oi  13910  fclim  15510  invf  17730  funcres2b  17859  funcres2c  17865  hofcllem  18219  hofcl  18220  nfchnd  18572  gsumval2  18649  resmgmhm2b  18676  resmhm2b  18785  frmdss2  18826  gsumval3a  19872  subgdmdprd  20005  srgfcl  20171  lsslindf  21808  indlcim  21818  cnrest2  23272  lmss  23284  conncn  23412  txflf  23992  cnextf  24052  clsnsg  24096  tgpconncomp  24099  psmetxrge0  24299  causs  25286  ellimc2  25865  perfdvf  25891  c1lip2  25986  dvne0  25999  plyeq0  26197  plyreres  26270  aannenlem1  26315  taylf  26347  ulmss  26383  elno2  27638  elno3  27639  cutsf  27804  madef  27848  oniso  28283  mpteleeOLD  28984  ausgrusgrb  29254  ausgrumgri  29256  usgrexmplef  29348  subuhgr  29375  subupgr  29376  subumgr  29377  subusgr  29378  upgrres  29395  umgrres  29396  hhssnv  31355  pjfi  31795  maprnin  32825  cycpmconjslem1  33237  esplyfv1  33763  measdivcstALTV  34419  sitgf  34541  eulerpartlemn  34575  reprinrn  34812  cvmlift2lem9a  35544  satff  35651  icoreresf  37727  poimirlem30  38030  poimirlem31  38031  isbnd3  38164  dihf11lem  41771  ofoafg  43812  ofoaid1  43816  ofoaid2  43817  naddcnff  43820  ntrf  44580  clsf2  44583  gneispace3  44590  gneispacef2  44593  k0004lem1  44604  dvsid  44788  stoweidlem27  46482  stoweidlem29  46484  stoweidlem31  46486  fourierdlem15  46577  mbfresmf  47194  sinnpoly  47366  ffnafv  47646  fcdmvafv2v  47711  iccpartf  47918  slotresfo  49401