Definition df-f 6531

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 7087, dff3 7088, and dff4 7089. (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 6523	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6522	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5648	. . . 4 class ran 𝐹
7	6, 2	wss 3898	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 401	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 209	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is used by:  feq1  6675  feq2  6676  feq3  6677  nff  6693  sbcfg  6695  ffn  6697  dffn2  6699  frn  6705  dffn3  6710  ffrnb  6712  fss  6714  fcof  6721  funssxp  6726  fdmrn  6729  fun  6732  fnfco  6735  fssres  6736  fcoi2  6745  fint  6749  fin  6750  f0  6751  fconst  6756  f1ssr  6774  fof  6784  dff1o2  6818  dff2  7087  dff3  7088  fmpt  7098  ffnfv  7107  ffvresb  7114  idref  7137  fpr  7146  dff1o6  7271  fliftf  7311  fiun  7938  f1iun  7939  ffoss  7941  1stcof  8014  2ndcof  8015  smores  8338  smores2  8340  iordsmo  8343  sbthlem9  9092  inf3lem6  9612  alephsmo  10152  alephsing  10325  axdc3lem2  10500  smobeth  10642  fpwwe2lem10  10696  gruiun  10855  gruima  10858  nqerf  10986  om2uzf1oi  14064  fclim  15687  invf  17904  funcres2b  18033  funcres2c  18039  hofcllem  18393  hofcl  18394  nfchnd  18746  mgmn0plusgf  18788  gsumval2  18836  resmgmhm2b  18863  resmhm2b  18979  frmdss2  19020  gsumval3a  20078  subgdmdprd  20211  srgfcl  20383  lsslindf  22097  indlcim  22107  cnrest2  23565  lmss  23577  conncn  23705  txflf  24286  cnextf  24346  clsnsg  24390  tgpconncomp  24393  psmetxrge0  24593  causs  25580  ellimc2  26158  perfdvf  26184  c1lip2  26279  dvne0  26292  plyeq0  26491  plyreres  26567  aannenlem1  26618  taylf  26651  ulmss  26687  elno2  27944  elno3  27945  cutsf  28111  madef  28155  oniso  28590  mpteleeOLD  29406  ausgrusgrb  29679  ausgrumgri  29681  usgrexmplef  29773  subuhgr  29800  subupgr  29801  subumgr  29802  subusgr  29803  upgrres  29820  umgrres  29821  hhssnv  31799  pjfi  32239  maprnin  33256  cycpmconjslem1  33648  esplyfv1  34134  measdivcstALTV  34791  sitgf  34913  eulerpartlemn  34947  reprinrn  35181  cvmlift2lem9a  35989  satff  36096  icoreresf  38195  poimirlem30  38488  poimirlem31  38489  isbnd3  38638  dihf11lem  42243  ofoafg  44299  ofoaid1  44303  ofoaid2  44304  naddcnff  44307  ntrf  45067  clsf2  45070  gneispace3  45077  gneispacef2  45080  k0004lem1  45091  dvsid  45259  stoweidlem27  46959  stoweidlem29  46961  stoweidlem31  46963  fourierdlem15  47054  mbfresmf  47671  ffnafv  48163  fcdmvafv2v  48228  iccpartf  48435  slotresfo  49929