We can have a shorter expression for AC by developing suggestions in a comment by Andreas to an answer by François and relying upon a proposal by Emil in the comments section: $\forall A(\forall a\forall b(a\in A\wedge b\in A\rightarrow (\exists x(x\in a\wedge x\in b)\leftrightarrow a=b))\rightarrow\exists T\forall a(a\in A\rightarrow\exists x\forall y(y=x\leftrightarrow y\in a\wedge y\in T)))$ Can we do better?