Skip to main content
4 of 6
Inessential change

We can have a shorter expression for AC by developing a suggestion in a comment by Andreas Blass to an answer by François:

$\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\forall b(a\in A\wedge b\in A\rightarrow(\exists x(x\in a\wedge x\in b\wedge x\in T)\leftrightarrow a=b))))$

Can we do better?