# Function from an expression

How do you formalize, in ZFC set theory, the process of forming a function from an expression?

Intuitively, I want to say something like this (I am guessing some vocabulary):

There is an expression $E$ with the only free variable $x$. When $x$ is substituted in $E$ with an element of a set $X$, the expression evaluates to an element $y_x$ of a set $Y$. Therefore, there exists a function $f_E : X \to Y$ such that $f_E(x) = y_x$.

The motivation is that I want to formalize the derivative of an expression, as in $D(x^2) = 2x$, where $x \in \mathbb{R}$. Here $E = x^2$, and the problem is to extract the implicitly-defined function $f_E : \mathbb{R} \to \mathbb{R}$ such that $f_E(x) = x^2$; the definition can then be reduced to that of the derivative of a function.

## 1 Answer

First note that the language of set theory has no constant symbols, or function symbols. So what $E$ really is, is a formula with free variables $x, y$ and possibly some parameters which are fixed, and for every $x\in X$ there is exactly one $y\in Y$ such that $E(x,y)$ is true in the universe.

So the set $f_E$ is really however you choose to represent functions on set theory, using $E$ to define it. For example if a function is a set of ordered pairs, then $f_E=\{\langle x, y\rangle\in X\times Y\mid E(x,y)\}$.

The parameters could be additional structure on $X$ or $Y$. Like addition, multiplication, topologies, etc.