Definition df-f 6437

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 6975, dff3 6976, and dff4 6977. (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 6429	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6428	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5590	. . . 4 class ran 𝐹
7	6, 2	wss 3887	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 396	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 205	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6581  feq2  6582  feq3  6583  nff  6596  sbcfg  6598  ffn  6600  dffn2  6602  frn  6607  dffn3  6613  ffrnb  6615  fss  6617  fcof  6623  fcoOLD  6625  funssxp  6629  fdmrn  6632  fun  6636  fnfco  6639  fssres  6640  fcoi2  6649  fint  6653  fin  6654  f0  6655  fconst  6660  f1ssr  6677  fof  6688  dff1o2  6721  dff2  6975  dff3  6976  fmpt  6984  ffnfv  6992  ffvresb  6998  idref  7018  fpr  7026  dff1o6  7147  fliftf  7186  fiun  7785  f1iun  7786  ffoss  7788  1stcof  7861  2ndcof  7862  smores  8183  smores2  8185  iordsmo  8188  sbthlem9  8878  inf3lem6  9391  alephsmo  9858  alephsing  10032  axdc3lem2  10207  smobeth  10342  fpwwe2lem10  10396  gruiun  10555  gruima  10558  nqerf  10686  om2uzf1oi  13673  fclim  15262  invf  17480  funcres2b  17612  funcres2c  17617  hofcllem  17976  hofcl  17977  gsumval2  18370  resmhm2b  18461  frmdss2  18502  gsumval3a  19504  subgdmdprd  19637  srgfcl  19751  lsslindf  21037  indlcim  21047  cnrest2  22437  lmss  22449  conncn  22577  txflf  23157  cnextf  23217  clsnsg  23261  tgpconncomp  23264  psmetxrge0  23466  causs  24462  ellimc2  25041  perfdvf  25067  c1lip2  25162  dvne0  25175  plyeq0  25372  plyreres  25443  aannenlem1  25488  taylf  25520  ulmss  25556  mptelee  27263  ausgrusgrb  27535  ausgrumgri  27537  usgrexmplef  27626  subuhgr  27653  subupgr  27654  subumgr  27655  subusgr  27656  upgrres  27673  umgrres  27674  hhssnv  29626  pjfi  30066  maprnin  31066  cycpmconjslem1  31421  measdivcstALTV  32193  sitgf  32314  eulerpartlemn  32348  reprinrn  32598  cvmlift2lem9a  33265  satff  33372  elno2  33857  elno3  33858  scutf  34006  madef  34040  icoreresf  35523  poimirlem30  35807  poimirlem31  35808  isbnd3  35942  dihf11lem  39280  ntrf  41733  clsf2  41736  gneispace3  41743  gneispacef2  41746  k0004lem1  41757  dvsid  41949  stoweidlem27  43568  stoweidlem29  43570  stoweidlem31  43572  fourierdlem15  43663  mbfresmf  44275  ffnafv  44663  frnvafv2v  44728  iccpartf  44883  resmgmhm2b  45354