How short can we state a principle which is equivalent with the Axiom of Choice under $ZF$? The principle should be a sentence in the language of set theory with only $\in$ and$=$ as extralogical relation signs; I thus disregard solutions that appeal to selectors as the epsilon operator. My motivation is to extend an interpretation of $ZF$ to one of $ZFC$, and a short sentence schema will make my work - simpler and shorter. 


Update: On the basis of comments I have developed an answer with a challenge as to whether we may improve. 



How short can we state the Axiom of Choice?
The following paper by Kurt Maes is focused on a version of the question at hand here, namely, finding an equivalent formulation of AC in the language of set theory using the fewest number of quantifiers, rather than merely the shortest length. In his main result, Maes finds a 5-quantifier assertion equivalent
to the axiom of choice. The statement is built on the same
statement as in François's answer, but modified to use fewer quantifiers (Maes has five, in comparison with ten for François; but of course François wasn't trying to minimize that quantity).


* Kurt Maes, [A 5-quantifier (\in,=)-expression ZF-equivalent to the Axiom of Choice](http://arxiv.org/abs/0705.3162).


Maes's result refuted a conjecture of Harvey
Friedman, which in the introduction the author mentions was stated on F.O.M., that it
would not be possible to state a formulation of the axiom of
choice using only five quantifiers.


Please see Maes's solution in his paper.


When I first heard about the Maes result (August 2004, apparently
an earlier draft of his paper—I haven't checked the
differences), I naturally set myself the task of proving the main result
myself, without looking at Maes's argument. I would encourage the same of all of you---before reading further, try to express AC in the language of set theory using only five quantifiers! Here is what I had come up with (retrieved after digging around in my old computer files):


**Theorem.** AC is equivalent (in ZF) to the following assertion:
 $$\forall A\exists B\forall a\in A\, \exists x\forall z$$
$$(x \in a \cap B) \wedge (z \in a \cap B \implies z=x) \wedge (a
\neq B)$$ $$\text{or }\quad(B \in x) \wedge (x \in A) \wedge (a
\neq x)$$ $$\text{or }\quad(B \in A) \wedge (z \notin B).$$


Proof. The point is that in order to get down to only five quantifiers, you have to essentially reuse the quantifiers to cover the various cases. The idea is that clause 1 expresses that $B$ is a selection
set
 for $A$, when $A$ is a family of disjoint nonempty sets (plus something extra useful when $A$ is not like that). Clause 2
 expresses that $A$ has elements that are not disjoint (at least two
 contain $B$). Clause 3 expresses that $A$ contains the emptyset
 ($B=\emptyset$).


AC easily implies the assertion. If $A$ is a family of disjoint nonempty
 sets, then we can let $B$ be a selection set for $A$, and verify clause 1. (note: in order to get $(a \neq B)$ in the case that $A$ is a singleton, we can freely add irrelevant elements to $B$ outside of $\bigcup A$.) If $A$ contains non-disjoint sets, we let $B$ be any element which is
 in at least two elements of $A$, and then we can always be in clause 2,
 since for any element of $A$ we can find another element of $A$ containing
 $B$. Finally, if $A$ contains the empty set, we can set $B=\emptyset$, and
 verify always clause 3.


Conversely, suppose that the stated principle holds. To prove AC, it
 suffices to construct a selection set for a family $A$ of disjoint
 non-empty sets. By replacing $A$ if necessary with the isomorphic copy
 $\{\{w\}\times a\mid a \in A\}$, where $w$ has high rank (such as $w=A$ itself), we
 may assume that every element of $\bigcup A$ has the same rank. Thus, every element of $A$ has rank one higher
 than this, and every element of $\bigcup\bigcup A$ has rank lower than
 this. It follows that no element of $\bigcup A$ is in $A$, and no element
 of $\bigcup A$ has itself elements in $\bigcup A$.


For such an $A$, we get $B$ by the stated principle. Note now that Clause
 2 implies $B \in\bigcup A$, and clause 3 implies $B \in A$. Meanwhile,
 clause 1 implies both that $B$ has an element in $\bigcup A$ and also that
 $B$ is not in $A$ (since it implies that $B\cap a$ is nonempty for
 some other $a\in A$, while sets in $A$ are disjoint). By our assumptions
 on $A$, these possibilities are mutually exclusive.
 It follows that $B$ must always be in clause 1, or always in clause 2,
 or always in clause 3, regardless of $a$, $x$, and $z$. If clause 3 always
 occurs, then $\emptyset\in A$, a contradiction. If clause 2 always
 occurs, then $B$ must be in more than one element of $A$, since otherwise
 we could let $a$ be that element, and this would contradict the
 disjointness of the elements of $A$. Thus, it must be that clause 1
 always occurs. In this case, $B$ is a selection set, and so we have
 established AC. QED


Although I am not aware of any utility flowing from the fact that AC can be exprssed in this manner, it is nevertheless true that proof theory has sometimes made advances by investigating the resource-limited expressive powers of languages. 


