Return to Answer

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?

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 below:

$\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?

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?

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?

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,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,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?

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?