Definition df-f 6359

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 6865, dff3 6866, and dff4 6867. (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 6351	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6350	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5556	. . . 4 class ran 𝐹
7	6, 2	wss 3936	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 398	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 208	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6495  feq2  6496  feq3  6497  nff  6510  sbcfg  6512  ffn  6514  dffn2  6516  frn  6520  dffn3  6525  fss  6527  fco  6531  funssxp  6535  fdmrn  6538  fun  6540  fnfco  6543  fssres  6544  fcoi2  6553  fint  6558  fin  6559  f0  6560  fconst  6565  f1ssr  6581  fof  6590  dff1o2  6620  dff2  6865  dff3  6866  fmpt  6874  ffnfv  6882  ffvresb  6888  idref  6908  fpr  6916  dff1o6  7032  fliftf  7068  fiun  7644  f1iun  7645  ffoss  7647  1stcof  7719  2ndcof  7720  smores  7989  smores2  7991  iordsmo  7994  sbthlem9  8635  inf3lem6  9096  alephsmo  9528  alephsing  9698  axdc3lem2  9873  smobeth  10008  fpwwe2lem11  10062  gruiun  10221  gruima  10224  nqerf  10352  om2uzf1oi  13322  fclim  14910  invf  17038  funcres2b  17167  funcres2c  17171  hofcllem  17508  hofcl  17509  gsumval2  17896  resmhm2b  17987  frmdss2  18028  gsumval3a  19023  subgdmdprd  19156  srgfcl  19265  lsslindf  20974  indlcim  20984  cnrest2  21894  lmss  21906  conncn  22034  txflf  22614  cnextf  22674  clsnsg  22718  tgpconncomp  22721  psmetxrge0  22923  causs  23901  ellimc2  24475  perfdvf  24501  c1lip2  24595  dvne0  24608  plyeq0  24801  plyreres  24872  aannenlem1  24917  taylf  24949  ulmss  24985  mptelee  26681  ausgrusgrb  26950  ausgrumgri  26952  usgrexmplef  27041  subuhgr  27068  subupgr  27069  subumgr  27070  subusgr  27071  upgrres  27088  umgrres  27089  hhssnv  29041  pjfi  29481  maprnin  30467  cycpmconjslem1  30796  measdivcstALTV  31484  sitgf  31605  eulerpartlemn  31639  reprinrn  31889  cvmlift2lem9a  32550  satff  32657  elno2  33161  elno3  33162  scutf  33273  icoreresf  34636  poimirlem30  34937  poimirlem31  34938  isbnd3  35077  dihf11lem  38417  ntrf  40522  clsf2  40525  gneispace3  40532  gneispacef2  40535  k0004lem1  40546  dvsid  40712  stoweidlem27  42361  stoweidlem29  42363  stoweidlem31  42365  fourierdlem15  42456  mbfresmf  43065  ffnafv  43419  frnvafv2v  43484  iccpartf  43640  resmgmhm2b  44116