Definition df-f 6566

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 7118, dff3 7119, and dff4 7120. (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 6558	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6557	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5689	. . . 4 class ran 𝐹
7	6, 2	wss 3962	. . 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  6716  feq2  6717  feq3  6718  nff  6732  sbcfg  6734  ffn  6736  dffn2  6738  frn  6743  dffn3  6748  ffrnb  6750  fss  6752  fcof  6759  funssxp  6764  fdmrn  6767  fun  6770  fnfco  6773  fssres  6774  fcoi2  6783  fint  6787  fin  6788  f0  6789  fconst  6794  f1ssr  6810  fof  6820  dff1o2  6853  dff2  7118  dff3  7119  fmpt  7129  ffnfv  7138  ffvresb  7144  idref  7165  fpr  7173  dff1o6  7294  fliftf  7334  fiun  7965  f1iun  7966  ffoss  7968  1stcof  8042  2ndcof  8043  smores  8390  smores2  8392  iordsmo  8395  sbthlem9  9129  inf3lem6  9670  alephsmo  10139  alephsing  10313  axdc3lem2  10488  smobeth  10623  fpwwe2lem10  10677  gruiun  10836  gruima  10839  nqerf  10967  om2uzf1oi  13990  fclim  15585  invf  17815  funcres2b  17947  funcres2c  17954  hofcllem  18314  hofcl  18315  gsumval2  18711  resmgmhm2b  18738  resmhm2b  18847  frmdss2  18888  gsumval3a  19935  subgdmdprd  20068  srgfcl  20213  lsslindf  21867  indlcim  21877  cnrest2  23309  lmss  23321  conncn  23449  txflf  24029  cnextf  24089  clsnsg  24133  tgpconncomp  24136  psmetxrge0  24338  causs  25345  ellimc2  25926  perfdvf  25952  c1lip2  26051  dvne0  26064  plyeq0  26264  plyreres  26338  aannenlem1  26384  taylf  26416  ulmss  26454  elno2  27713  elno3  27714  scutf  27871  madef  27909  mptelee  28924  ausgrusgrb  29196  ausgrumgri  29198  usgrexmplef  29290  subuhgr  29317  subupgr  29318  subumgr  29319  subusgr  29320  upgrres  29337  umgrres  29338  hhssnv  31292  pjfi  31732  maprnin  32748  cycpmconjslem1  33156  measdivcstALTV  34205  sitgf  34328  eulerpartlemn  34362  reprinrn  34611  cvmlift2lem9a  35287  satff  35394  icoreresf  37334  poimirlem30  37636  poimirlem31  37637  isbnd3  37770  dihf11lem  41248  ofoafg  43343  ofoaid1  43347  ofoaid2  43348  naddcnff  43351  ntrf  44112  clsf2  44115  gneispace3  44122  gneispacef2  44125  k0004lem1  44136  dvsid  44326  stoweidlem27  45982  stoweidlem29  45984  stoweidlem31  45986  fourierdlem15  46077  mbfresmf  46694  ffnafv  47120  fcdmvafv2v  47185  iccpartf  47355