Definition df-f 6515

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 7071, dff3 7072, and dff4 7073. (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 6507	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6506	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5639	. . . 4 class ran 𝐹
7	6, 2	wss 3914	. . 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  6666  feq2  6667  feq3  6668  nff  6684  sbcfg  6686  ffn  6688  dffn2  6690  frn  6695  dffn3  6700  ffrnb  6702  fss  6704  fcof  6711  funssxp  6716  fdmrn  6719  fun  6722  fnfco  6725  fssres  6726  fcoi2  6735  fint  6739  fin  6740  f0  6741  fconst  6746  f1ssr  6762  fof  6772  dff1o2  6805  dff2  7071  dff3  7072  fmpt  7082  ffnfv  7091  ffvresb  7097  idref  7118  fpr  7126  dff1o6  7250  fliftf  7290  fiun  7921  f1iun  7922  ffoss  7924  1stcof  7998  2ndcof  7999  smores  8321  smores2  8323  iordsmo  8326  sbthlem9  9059  inf3lem6  9586  alephsmo  10055  alephsing  10229  axdc3lem2  10404  smobeth  10539  fpwwe2lem10  10593  gruiun  10752  gruima  10755  nqerf  10883  om2uzf1oi  13918  fclim  15519  invf  17730  funcres2b  17859  funcres2c  17865  hofcllem  18219  hofcl  18220  gsumval2  18613  resmgmhm2b  18640  resmhm2b  18749  frmdss2  18790  gsumval3a  19833  subgdmdprd  19966  srgfcl  20105  lsslindf  21739  indlcim  21749  cnrest2  23173  lmss  23185  conncn  23313  txflf  23893  cnextf  23953  clsnsg  23997  tgpconncomp  24000  psmetxrge0  24201  causs  25198  ellimc2  25778  perfdvf  25804  c1lip2  25903  dvne0  25916  plyeq0  26116  plyreres  26190  aannenlem1  26236  taylf  26268  ulmss  26306  elno2  27566  elno3  27567  scutf  27724  madef  27764  onsiso  28169  mptelee  28822  ausgrusgrb  29092  ausgrumgri  29094  usgrexmplef  29186  subuhgr  29213  subupgr  29214  subumgr  29215  subusgr  29216  upgrres  29233  umgrres  29234  hhssnv  31193  pjfi  31633  maprnin  32654  cycpmconjslem1  33111  measdivcstALTV  34215  sitgf  34338  eulerpartlemn  34372  reprinrn  34609  cvmlift2lem9a  35290  satff  35397  icoreresf  37340  poimirlem30  37644  poimirlem31  37645  isbnd3  37778  dihf11lem  41260  ofoafg  43343  ofoaid1  43347  ofoaid2  43348  naddcnff  43351  ntrf  44112  clsf2  44115  gneispace3  44122  gneispacef2  44125  k0004lem1  44136  dvsid  44320  stoweidlem27  46025  stoweidlem29  46027  stoweidlem31  46029  fourierdlem15  46120  mbfresmf  46737  sinnpoly  46892  ffnafv  47172  fcdmvafv2v  47237  iccpartf  47432  slotresfo  48887