The bold statement is not true in the generality in which you
state it.

But let's get a little more clear on what you mean. One does not
formally use axioms at all in a *definition*, but rather in a
proof. I suppose what one means by using an axiom in a definition,
is that certain claims are being made about the defined object, such as
that it exists and is the unique thing satisfying some property
(the definition), or perhaps that one undertook a constructive
procedure, which is really just a sequence of such definitions.
Such a construction could be said to not use the axiom of choice,
if at every step, in every model of ZF the definition succeeds in
defining a unique object.

It is easy to make a counterexample, now, by the definition: let
$f$ be the characteristic function of the $L$-least non-measurable
set of reals in $L$.

This definition does not use the axiom of choice, since it is
sensible as a definition in any model of ZF, and picks out a
unique function on the reals in any model of ZF. But it is not
provable in ZF that this function is measurable, since if $V=L$,
then $f$ is definitely non-measurable.

Meanwhile, it is consistent with ZFC that the set of all reals in
$L$ is countable in $V$, and in this case, the function $f$ is the
characteristic of a countable set, and hence measurable in $V$.

So the definition, which did not use the axiom of choice (since it
works as a definition in any model of ZF), sometimes defines a
measurable function and sometimes does not, in the various ZF
worlds.

At the end of your post, you seem to suggest that, ("clearly") if a definition
defines a measurable set in some model of ZF, then it defines a
measurable set (in our current ZFC universe). But this is not
quite right. One can write down a definition $\varphi(x)$ that ZF proves defines a unique set of reals, but the set of reals defined is measurable in an inner model and non-measurable in a larger model. 

Lastly, let me mention that there is another sense in which
something very like your bold statement is true, and so actually
you are not too far off, if you adopt the perspective and
philosophy of large cardinal set theory. Namely, if there are
sufficient large cardinals, then it follows that every
projectively definable function or set of reals is Lebesgue
measurable. A projectively definable set is one that defines the
set or function by quantifying only over the reals and the
integers and the basic algebraic operations and orders there. It
goes beyond projective, and I see now that Andres has posted some
further links on this.