Does "if" turn a free variable into a bound variable? A closed formula expresses a proposition (which is a truth-apt concept, so a concept that is either be "true" or "false"). A closed formula is a Boolean-valued formula with no free variables.
A free variable is a variable that "specifies places in an expression where substitution may take place and is not a parameter of this or any container expression", it has not been bound by a variable-binding operator like
$$
\sum _{x\in S}\quad \quad \prod _{x\in S}\quad \quad \int _{0}^{\infty }\cdots \,dx\quad \quad \lim _{x\to 0}\quad \quad \forall x\quad \quad \exists x
$$
So for example (in the following all numbers, variables, and function values are real numbers)
\begin{align}
f(x) = 5, f(x) = 2*x \qquad\qquad\qquad\qquad\qquad (1)
\end{align}
is not true or false, as long as we don't know what $x$ is. But if we say,
$$
\text{if } x = 2, f(x) = 2*x \text{, then } f(x) = 5 \qquad\;\;\qquad (2)
$$
this becomes truth-apt (in this case this is false). So, I would think that "if" is a variable-binding operator. Is this correct?
Another way of writing "if" is by using $\Rightarrow$, e.g.,
$$
x = 2, f(x) = 2*x \Rightarrow f(x) = 5 \qquad\qquad\qquad (3)
$$
which I would think is a closed formula which is false.
 A: 
\begin{align}
f(x) = 5\text{ and } f(x) = 2x\tag1
\end{align}
is not true or false, as long as we don't know what $x$ is.
$$\text{if } x = 2\text{ and } f(x) = 2x \text{, then } f(x) = 5\tag2$$
this becomes truth-apt (in this case this is false). So, I would think that "if" is a variable-binding operator. Is this correct?

Has $f$ been pre-defined such that $f(x)=2x\,?$ If so, then the open formula $(2)$ is actually true for all values of $x$ except $2.5.$ What is false though is the closed formula $$\text{for each $x,\Big($if } x = 2\text{ and } f(x) = 2x \text{, then } f(x) = 5\Big)\tag{2a}.$$ Informally, open conditional formulae like $(2)$ are typically treated as closed formulae like $(2a);$ it is this implicit universal quantification—not the conditional operator per se—that binds the free variable $x.$
On the other hand, if $f(x)$ actually equals, say, $-\dfrac1x,$ then both formulae $(2)$ and $(2a)$ are definitely true in the standard interpretation.
A: Actually, we do not need variable-bounding in this instance; quantifier-free fragment of first-order logic with equality (see Ian Chiswell and Wilfrid Hodges' Mathematical Logic, chapter 5) or equational logic will do.
We can take the signature as
$\sigma_{eq} = \langle \mathcal{A}, a, b, c,\ldots f, g, h,\ldots =, R, S,\ldots\rangle$
where $\mathcal{A}$ is a set as the domain of discourse; $a, b, c,\ldots$ are individual constants; $f, g, h,\ldots$ are (term-forming) functions; $=, R, S,\ldots$ are relations (representing predicates in the domain). '$=$' is the equality relation, it can be put into the logical vocabulary into the signature.
The functions can be represented as
$\phi$ as $=\!(x, 2)$, $\psi$ as $=\!(f(x), 2)$, $\upsilon$ as $=\!(f(x), 5)$.
Natural deduction system with the '=' introduction rule
$\dfrac{}{t=t}\;\;\; (=I)$
and '=' elimination rule
$\dfrac{s = t\;\;\;\;\phi(s/x)}{\phi(t/x)}\;\;\; (=E)$
together with the equality axioms of reflexivity, symmetry, and transitivity, will suffice.
A significant point in this perspective is that free variables are not merely syntactic elements. They are also semantic constituents that serve roughly as names or parameters in a fashion comparable to logical names in computer science for which we have not specified definite physical names.
