A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$
I would recommend looking at higher-order logics (HOL), for instance Lambek and Scott's Introduction to Higher-Order Categorical Logic. Such a logic will set up binding of bound variables and treat variable contexts properly (single-sorted first-order logic tends to have a somewhat simplistic view of those).

Note that your suggestion to always bind just a single variable does not cover operators that require simulatneous binding of several variables. They are uncommon, but do appear occasionally.

To get what you're asking for, we can cut down on the order. In HOL there is a single sort of types, including a type of propositions $\Omega$, which are closed under formation of function spaces, so that higher-order predicates are formed as $\Omega$, $A \to \Omega$, $(A \to \Omega) \to \Omega$. To prevent these, we can stratify the types into several sorts:


the sort of primitive types $A$, $B$, $C$, ... (in first-order logic you often have just a single one, which is not mentioned at all) 
the sort of propositions $\Omega$
the sort of first-order functions $(A_1, \ldots, A_n) \to B$, where $A_i$ and $B$ are primitive types
the sort of (first-order) propositional functions $(A_1, \ldots, A_n) \to \Omega$, where $A_i$ are primitive types.


Variables always range over primitive types. A context $\Gamma$ is a list of variables with their (primitive) types, $\Gamma \equiv x_1 : A_1, \ldots, x_n : A_n$. We never speak of an expression without specifying its context, so that we can keep track of which variables are allowed to appear.

If $S$ is a sort, we write $\Gamma \vdash e : S$ when $e$ is an expression of sort $S$ in context $\Gamma$. For example,
$$x : \mathbb{R}, y : \mathbb{R} \vdash (\exists z : \mathbb{R} . x + z = y) : \Omega$$
is the assertion that $\exists z : \mathbb{R} . x + z = y$ is a proposition (in the given context). It is not the assertion that $\exists z : \mathbb{R} . x + z = y$ holds! For that we postulate a new judgement of the form
$$\Gamma \mid \theta_1, \ldots, \theta_n \vdash \psi \ \mathsf{true}
\tag{1}$$
which states, intuitively, that propositions $\theta_1, \ldots, \theta_n$ jointly entail the proposition $\psi$. If we also have equations (at all types), (1) can be replaced with
$$\Gamma \mid (\theta_1 \land \cdots \land \theta_n) \land \psi =_\Omega \theta_1 \land \cdots \land \theta_n.$$
This is the approach taken by Lambek and Scott. Its main advantage is that the formal system is more like algebra, since it is just a bunch of (fancy) operations and equations.

Another example (where I am using the notation $\langle x_1 : A_1, \ldots, x_n : A_n \rangle . e$ to express the fact that the variables $x_1, \ldots, x_n$ are bound in $e$):
$$x : \mathbb{R} \vdash (\langle y : \mathbb{R}, z : \mathbb{R} \rangle . y^2 + x \cdot z) : (\mathbb{R}, \mathbb{R}) \to \mathbb{R}.$$ 
This says that there is a function taking $(y, z)$ to $y^2 + x \cdot z$.

We can now introduce first-order binders as operations that map first-order (propositional) functions to primitive sorts and propositions, for instance:


$\forall$ is an operation which takes a propositional function $(A) \to \Omega$ to a proposition. The formation rule would read as follows:
$$\frac{\Gamma \vdash p : (A) \to \Omega}{\Gamma \vdash \forall p : \Omega}$$
En example of such an expression would be $\forall (\langle x : \mathbb{R} \rangle . x^4 - 5 x^2 + 7 &gt; 0)$.
Assuming there is a primitive type $\mathsf{Set}$ of sets and a relation symbol $\in$ of sort $(\mathsf{Set}, \mathsf{Set}) \to \Omega$, subset formation $\sigma$ is an operation which takes $s : \mathsf{Set}$ and $p : (\mathsf{Set}) \to \Omega$ and yields $\sigma(s, p) : \mathsf{Set}$. We also need some rules regarding these, e.g.,
$$
\Gamma \mid \vec{\theta}, e \in s, p(s) \vdash e \in \sigma(s, p) \ \mathsf{true}.
$$
We can also do unrestricted comprehension $\sigma'$, the kind that leads to Russell's paradox. It takes $p : (\mathsf{Set}) \to \Omega$ to $\sigma' p : \mathsf{Set}$. Assuming there is also $\epsilon : (\mathsf{Set}, \mathsf{Set}) \to \Omega$ and negation, we can define Russell's paradoxical $R$ as $\sigma' (\langle x : \mathsf{Set} \rangle . \lnot (x \in x))$.
For a "non-logical" example, let us introduce the $\lambda$-notation from $\lambda$-calculus. Suppose for every primitive types $A$ and $B$ there is a primitive type $A \Rightarrow B$ (normally written as $A \to B$ but I am using a different arrow to avoid confusion). For all primitive types $A$ and $B$, we can introduce an operator $\lambda_{A, B}$ which takes $f : (A) \to B$ to an expression $\lambda_{A,B} f : A \Rightarrow B$. The identity map on $A$ is thus written as $\lambda_{A,A} (\langle x : A \rangle . x)$. This is an example of a higher-order calculus of types with first-order logic layered on top of it (as opposed to HOL, where $\Omega$ is mixed with $\Rightarrow$ freely).


I do not know of any texts that would carefully developed this sort of calculus. I do not know why that is. Traditional logic textbooks usually simplify matters by considering a single-sorted first-order language, whereas the newer computer-sciency texts dive for fancier stuff with unrestricted order. You're asking for a bastard child of higher-order logic, I suppose.