# Formal Dirichlet-Bourbaki definition of function

What is the formal Dirichlet-Bourbaki definition of a function?

I have come across this in this essay: http://www.k-12prep.math.ttu.edu/journal/contentknowledge/meel01/article.pdf on page 1.

I know what a function is and I can write down a definition. What I would like to know is what the the definition is that is specifically known as the formal Dirichlet-Bourbaki definition.

A function $f:X\rightarrow Y$ is a subset of $X\times Y$ such that $(x,y_1)\in f$ and $(x,y_2)\in f$ implies $y_1=y_2$.
• You left out $\forall x\in X\;\exists y\;(\;(x,y)\in f).$ – DanielWainfleet Apr 7 '16 at 17:55