Measurability and Axiom of choice In some situations, you need to show Lebesgue-measurability of some function on $\mathbb{R}^n$ and the verification is kind of lengthy and annoying, and even more so because measurability is "obvious" because "why would it not be".
In such a situation, I have heard the argument: The function is clearly measurable, because the axiom of choice was not used to define it.
This argument makes some sense, because (as far as I know, I am not an expert) there are models of ZF (no C), where every function on $\mathbb{R}^n$ is Lebesgue measurable. So, suppose that we have a function $f$ in our model of ZFC constructed without the axiom of choice, then it is also a function in the model of ZF constructed above. Hence it is measurable there, and "clearly" all functions that are measurable in the model above are also measurable in our model.
But the question is: The bold statement above is very "meta". So how rigorous is this argument? Can it be made rigorous?
/Edit: I changed "Borel"- to "Lebesgue"-Measurable.
 A: Analytic sets that are not Borel can be explicitly defined.  AC is not used in the definition.  It is only the proof that they are not Borel that requires AC.
However: Lebesgue measurable is much more like your description.
A: The bold statement is not true in the generality in which you
state it. Nevertheless, something very like it is true, if one
adopts the perspective and philosophy of large cardinal set theory
and restricts the kinds of definitions that are considered.
First, 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. To define an object means to provide a statement
$\varphi(x)$ that one and only one object satisfies. What one
means by not using an axiom in a definition, is that one can
prove, without using that axiom, that there is such a unique
object fulfilling the definition. Perhaps one has in mind a
constructive procedure, but this is really just a sequence of such
definitions, and such a construction does not use the axiom of
choice, if at every step of the construction, the definition used
at that step is a definition in any model of ZF.
One can easily make a counterexample, now, by the definition: let
$f$ be the characteristic function of the least non-measurable set
of reals in the constructible universe $L$, using the canonical 
definable well-ordering of $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
necessarily true in ZF that this function is measurable, since if
the axiom of constructibility holds, that is, if we are living in
$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, sometimes
defines a measurable function and sometimes does not, in the
various ZF worlds.
Let's give another concrete counterexample. The canonical
well-ordering of the reals in the constructible universe $L$, mentioned by Andres,
is a definable subset of the real plane $A\subset\mathbb{R}^2$,
which in $L$ has complexity $\Delta^1_2$ in the descriptive-set-theoretic
projective hierarchy. Thus, in our current universe $V$, the set $A$ has complexity at worst $\Sigma^1_2$, and so it arises from a certain definable
closed subset of $\mathbb{R}^4$ by projecting onto $\mathbb{R}^3$,
taking the complement, and then projecting to $\mathbb{R}^2$. So $A$ is definable in a highly concrete manner, without
making any use of the axiom of choice. Nevertheless, it is not
necessarily true that the resulting set is measurable, since
inside the constructible universe itself, the resulting set is not
measurable; in contrast, it is also consistent with ZF that there
are only countably many constructible reals, and in this case the
set $A$ would be countable and hence measurable. So the
measurability of the set $A$ is not determined, despite the simple
definition.
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 explain the sense in which your bold statement is
on the right track. One of the truly surprising and remarkable
discoveries of large cardinal set theory is that the existence of
large cardinals has effects on fundamental mathematical truth at
the level of descriptive set theory. In particular, the existence
of sufficient large cardinals implies that every projectively
definable set of reals is Lebesgue measurable. If there is a
supercompact cardinal, and much less suffices, as explained in the
article Saharon Shelah, Hugh Woodin, Large Cardinals Imply That
Every Reasonably Definable Set of Reals Is Lebesgue Measurable,
Isreal Journal of Mathematics, vol. 70, (1990) pp. 381-394 (reviewed by J. Bagaria in BSL 8:4(2002) pp. 543-545, as linked to by Andres in the comments), then every
set of reals in $L(\mathbb{R})$ is Lebesgue measurable. The universe $L(\mathbb{R})$ consists of those sets that are constructible relative to reals.
So, if you assume large cardinals, and you define a set of reals
by a definition that is absolute to $L(\mathbb{R})$ — and
this is very likely the case if your definition works in ZF and
does not involve set theory explicitly — then your set is
Lebesgue measurable.
In particular, assuming that there are sufficient large cardinals, then every projective set of reals is Lebesgue measurable, and this may provide a soft sufficient criterion. The projective statements are those that can be expressed using quantifiers only over the reals and the integers, with the usual algebraic and order structure. Alternatively, the projective sets are those that you get by closing the Borel sets under continuous images and complements. 
Let me point out that this kind of consequence of large cardinals
is often pointed to by large cardinal set theorists as evidence
that the large cardinal axioms themselves are on the right track,
since they provide a such a rich, coherent and desirable structure
theory for our everyday mathematics. We infinitely prefer the
smooth and elegant descriptive set theory of large cardinals to
the awkward land of counterexamples provided by the axiom of
constructibility $V=L$.
