Definition df-f 5793

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 6263, dff3 6264, and dff4 6265. (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 5785	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5784	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5028	. . . 4 class ran 𝐹
7	6, 2	wss 3539	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 382	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 194	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5924  feq2  5925  feq3  5926  nff  5939  sbcfg  5941  ffn  5943  dffn2  5945  frn  5951  dffn3  5952  fss  5954  fco  5956  funssxp  5959  fdmrn  5962  fun  5964  fnfco  5966  fssres  5967  fcoi2  5976  fint  5981  fin  5982  f0  5983  fconst  5988  f1ssr  6004  fof  6012  dff1o2  6039  dff2  6263  dff3  6264  fmpt  6273  ffnfv  6279  ffvresb  6285  fpr  6303  idref  6380  dff1o6  6408  fliftf  6442  fun11iun  6996  ffoss  6997  1stcof  7064  2ndcof  7065  smores  7313  smores2  7315  iordsmo  7318  sbthlem9  7940  sucdom2  8018  inf3lem6  8390  alephsmo  8785  alephsing  8958  axdc3lem2  9133  smobeth  9264  fpwwe2lem11  9318  gch3  9354  gruiun  9477  gruima  9480  nqerf  9608  om2uzf1oi  12571  fclim  14080  invf  16199  funcres2b  16328  funcres2c  16332  hofcllem  16669  hofcl  16670  gsumval2  17051  resmhm2b  17132  frmdss2  17171  gsumval3a  18075  subgdmdprd  18204  srgfcl  18286  lsslindf  19935  indlcim  19945  cnrest2  20847  lmss  20859  concn  20986  txflf  21567  cnextf  21627  clsnsg  21670  tgpconcomp  21673  psmetxrge0  21875  causs  22848  ellimc2  23391  perfdvf  23417  c1lip2  23509  dvne0  23522  plyeq0  23715  plyreres  23786  aannenlem1  23831  taylf  23863  ulmss  23899  mptelee  25520  ausisusgra  25677  usgraedgrnv  25699  usgraexmplef  25722  cusgrarn  25781  hhssnv  27298  pjfi  27740  maprnin  28687  measdivcstOLD  29407  sitgf  29529  eulerpartlemn  29563  cvmlift2lem9a  30332  elno2  30844  elno3  30845  nodenselem6  30878  icoreresf  32159  poimirlem30  32392  poimirlem31  32393  isbnd3  32536  dihf11lem  35356  ntrf  37224  clsf2  37227  gneispace3  37234  gneispacef2  37237  gneispacern  37239  k0004lem1  37248  dvsid  37335  stoweidlem27  38703  stoweidlem29  38705  stoweidlem31  38707  fourierdlem15  38798  mbfresmf  39409  ffnafv  39684  iccpartf  39753  ausgrusgrb  40376  ausgrumgri  40378  subuhgr  40491  subupgr  40492  subumgr  40493  subusgr  40494  resmgmhm2b  41571