Definition df-f 6506

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 7055, dff3 7056, and dff4 7057. (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 6498	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6497	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5635	. . . 4 class ran 𝐹
7	6, 2	wss 3903	. . 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  6650  feq2  6651  feq3  6652  nff  6668  sbcfg  6670  ffn  6672  dffn2  6674  frn  6679  dffn3  6684  ffrnb  6686  fss  6688  fcof  6695  funssxp  6700  fdmrn  6703  fun  6706  fnfco  6709  fssres  6710  fcoi2  6719  fint  6723  fin  6724  f0  6725  fconst  6730  f1ssr  6746  fof  6756  dff1o2  6789  dff2  7055  dff3  7056  fmpt  7066  ffnfv  7075  ffvresb  7082  idref  7103  fpr  7111  dff1o6  7233  fliftf  7273  fiun  7899  f1iun  7900  ffoss  7902  1stcof  7975  2ndcof  7976  smores  8296  smores2  8298  iordsmo  8301  sbthlem9  9037  inf3lem6  9556  alephsmo  10026  alephsing  10200  axdc3lem2  10375  smobeth  10511  fpwwe2lem10  10565  gruiun  10724  gruima  10727  nqerf  10855  om2uzf1oi  13890  fclim  15490  invf  17706  funcres2b  17835  funcres2c  17841  hofcllem  18195  hofcl  18196  nfchnd  18548  gsumval2  18625  resmgmhm2b  18652  resmhm2b  18761  frmdss2  18802  gsumval3a  19849  subgdmdprd  19982  srgfcl  20148  lsslindf  21802  indlcim  21812  cnrest2  23247  lmss  23259  conncn  23387  txflf  23967  cnextf  24027  clsnsg  24071  tgpconncomp  24074  psmetxrge0  24274  causs  25271  ellimc2  25851  perfdvf  25877  c1lip2  25976  dvne0  25989  plyeq0  26189  plyreres  26263  aannenlem1  26309  taylf  26341  ulmss  26379  elno2  27639  elno3  27640  cutsf  27805  madef  27849  oniso  28284  mpteleeOLD  28986  ausgrusgrb  29256  ausgrumgri  29258  usgrexmplef  29350  subuhgr  29377  subupgr  29378  subumgr  29379  subusgr  29380  upgrres  29397  umgrres  29398  hhssnv  31358  pjfi  31798  maprnin  32827  cycpmconjslem1  33254  esplyfv1  33752  measdivcstALTV  34409  sitgf  34531  eulerpartlemn  34565  reprinrn  34802  cvmlift2lem9a  35525  satff  35632  icoreresf  37634  poimirlem30  37930  poimirlem31  37931  isbnd3  38064  dihf11lem  41671  ofoafg  43740  ofoaid1  43744  ofoaid2  43745  naddcnff  43748  ntrf  44508  clsf2  44511  gneispace3  44518  gneispacef2  44521  k0004lem1  44532  dvsid  44716  stoweidlem27  46414  stoweidlem29  46416  stoweidlem31  46418  fourierdlem15  46509  mbfresmf  47126  sinnpoly  47280  ffnafv  47560  fcdmvafv2v  47625  iccpartf  47820  slotresfo  49287