Does this formalism adequately describe functions of one variable? Let $f$ be a function mapping every element of a set $X$ to a unique element denoted by $f(x)$ in a set $Y$.
Can this statement be effectively formalized by 

$\forall a (a\in X \implies f(a) \in Y)$

What logical aspects of functionality, if any, would not be captured by this statement. 
 A: For a more or less standard FOL, as is typically used to formalize, e.g., ZFC set theory, writing $f(a)$ already implies that $f$ is a function. Your statement would merely add that the image of $X$ is contained in $Y$. If that's all you want, then this is fine.
Fixing $a\in X$, if $f$ is a set-theoretic function, as opposed to a logical function symbol, then $f(a)\in Y$ would mean something like $\exists y\in Y.(a,y)\in f$. This would imply $f$ is a total relation on $X$, but not that it is functional which would just add that such a $y$ has to be unique. This is the point of Randall's comments. Without the uniqueness constraint, $f$ could readily be a relation that relates $a$ to multiple elements of $Y$. Your argument that you can "trivially" show $f(a)=f(a)$ doesn't work when $f$ is not a function symbol. There is no term $f(a)$ in this context.1 Instead $f(x)=y$ is interpreted as $(x,y)\in f$, so in your case you'd get $f(a)=f(a)$ means $(a,f(a))\in f$ means $\exists b.(a,b)\in f\land(a,b)\in f$ which is, of course, equivalent to just $\exists b.(a,b)\in f$ which in no way states that that $b$ is unique.
$f$ may still not be a function since we haven't said anything about how it behaves outside of $X$. You can add an additional constraint: $\forall a,b.(a,b)\in f\implies a\in X$ which would say that $f$ is only "defined" on $X$. In APC89's answer, this is accomplished by requiring $f\subset X\times Y$.
If you just want to specify that a binary relation $f$ is a function $X$ to $Y$, then APC89's answer provides the more or less standard definition for this, except for the unnecessary insistence that $X$ and $Y$ be non-empty. (Of course, if $Y$ is empty and $X$ is non-empty, there won't actually be any functions from $X$ to $Y$. On the other hand, $X$ being empty causes no problems at all.)
1 If your logic has a definite description quantifier, you could say it is the term $\iota b.(a,b)\in f$, but this also would require $f$ to separately be shown to be a functional relation for this to give a useful result.
A: Given two non-empty sets $A$ and $B$, we say that the binary relation $f\subset A\times B$ is a function from $A$ to $B$ if and only if
\begin{align*}
(\forall a\in A)(\exists!b\in B)\quad\text{such that}\quad(a,b)\in f
\end{align*}
A: If the symbols $f$, $X$, and $Y$ are established to be interpreted so that $f$ is a function and $X,Y$ are sets, then your formalism captures $X\subseteq \mathrm{dom}(f)$ and $\mathrm{ran}(f\big|_X)\subseteq Y$. It does not establish that $f$ is a function and $X,Y$ are sets---that must be established before writing the formalism.
