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.