Definition df-f 6491

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 7040, dff3 7041, and dff4 7042. (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 6483	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6482	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5621	. . . 4 class ran 𝐹
7	6, 2	wss 3885	. . 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  6635  feq2  6636  feq3  6637  nff  6653  sbcfg  6655  ffn  6657  dffn2  6659  frn  6664  dffn3  6669  ffrnb  6671  fss  6673  fcof  6680  funssxp  6685  fdmrn  6688  fun  6691  fnfco  6694  fssres  6695  fcoi2  6704  fint  6708  fin  6709  f0  6710  fconst  6715  f1ssr  6731  fof  6741  dff1o2  6774  dff2  7040  dff3  7041  fmpt  7051  ffnfv  7060  ffvresb  7067  idref  7088  fpr  7097  dff1o6  7219  fliftf  7259  fiun  7885  f1iun  7886  ffoss  7888  1stcof  7961  2ndcof  7962  smores  8281  smores2  8283  iordsmo  8286  sbthlem9  9022  inf3lem6  9543  alephsmo  10013  alephsing  10187  axdc3lem2  10362  smobeth  10498  fpwwe2lem10  10552  gruiun  10711  gruima  10714  nqerf  10842  om2uzf1oi  13904  fclim  15504  invf  17724  funcres2b  17853  funcres2c  17859  hofcllem  18213  hofcl  18214  nfchnd  18566  gsumval2  18643  resmgmhm2b  18670  resmhm2b  18779  frmdss2  18820  gsumval3a  19867  subgdmdprd  20000  srgfcl  20166  lsslindf  21799  indlcim  21809  cnrest2  23239  lmss  23251  conncn  23379  txflf  23959  cnextf  24019  clsnsg  24063  tgpconncomp  24066  psmetxrge0  24266  causs  25253  ellimc2  25832  perfdvf  25858  c1lip2  25953  dvne0  25966  plyeq0  26164  plyreres  26237  aannenlem1  26282  taylf  26314  ulmss  26350  elno2  27606  elno3  27607  cutsf  27772  madef  27816  oniso  28251  mpteleeOLD  28952  ausgrusgrb  29222  ausgrumgri  29224  usgrexmplef  29316  subuhgr  29343  subupgr  29344  subumgr  29345  subusgr  29346  upgrres  29363  umgrres  29364  hhssnv  31323  pjfi  31763  maprnin  32792  cycpmconjslem1  33203  esplyfv1  33701  measdivcstALTV  34357  sitgf  34479  eulerpartlemn  34513  reprinrn  34750  cvmlift2lem9a  35473  satff  35580  icoreresf  37656  poimirlem30  37959  poimirlem31  37960  isbnd3  38093  dihf11lem  41700  ofoafg  43770  ofoaid1  43774  ofoaid2  43775  naddcnff  43778  ntrf  44538  clsf2  44541  gneispace3  44548  gneispacef2  44551  k0004lem1  44562  dvsid  44746  stoweidlem27  46443  stoweidlem29  46445  stoweidlem31  46447  fourierdlem15  46538  mbfresmf  47155  sinnpoly  47327  ffnafv  47607  fcdmvafv2v  47672  iccpartf  47879  slotresfo  49362