There is The Epsilon Calculus developed by David Hilbert during the 20s.

It is based on the $\epsilon$ simbol :

if $A$ is a formula and $x$ is a variable, $εx \ A$ is a term

with the axiom (Hilbert's “transfinite axiom”) :

$A(x) → A(εx A)$.

The intended interpretation is that $εx \ A$ denotes some $x$ satisfying $A$, if there is one.

Quantifiers can be defined as follows:

$∃x A(x) ≡ A(εx A)$

$∀x A(x) ≡ A(εx (¬A)).$

See the use of epsilon notation in Nicolas Bourbaki, Elements of Mathematics : Theory of sets (1968 - French ed. 1958), page 20 and page 36.

There is The Epsilon Calculus developed by David Hilbert during the 20s.

It is based on the $ε$ symbol :

if $A$ is a formula and $x$ is a variable, $εx \ A$ is a term

with the axiom (Hilbert's “transfinite axiom”) :

$A(x) → A(εx A)$.

The intended interpretation is that $εx \ A$ denotes some $x$ satisfying $A$, if there is one.

Quantifiers can be defined as follows:

$∃x A(x) ≡ A(εx A)$

$∀x A(x) ≡ A(εx (¬A)).$

See the use of epsilon notation in Nicolas Bourbaki, Elements of Mathematics : Theory of sets (1968 - French ed. 1958), page 20 and page 36 [with $\tau_x$ in place of $εx$].