Cet axiome fait partie des axiomes optionnels et controversés de la théorie des ensembles. En effet, l'existence d'un objet défini à partir de l'axiome du choix n'est pas une existence constructive, c’est-à-dire que l'axiome ne décrit aucunement comment construire l'objet dont on affirme l'existence. Ainsi, dire qu'il existe une base de l'espace vectoriel des fonctions continues de R dans R ne permet en aucune façon de décrire une telle base. De ce point de vue, l'axiome du choix peut paraître d'un intérêt limité et c'est pourquoi certains mathématiciens se montrent plus satisfaits d'une démonstration s'ils peuvent éviter d'avoir recours à cet axiome du choix. Mais la plupart des mathématiciens l'utilisent sans réticence particulière.
L'axiome du choix ne fait pas partie du jeu d'axiomes de la théorie des ensembles ZF. On appelle théorie ZFC, la théorie ZF munie en plus de l'axiome du choix.
L'axiome du choix est souvent utilisé par l'intermédiaire de l'un des deux énoncés suivants qui lui sont équivalents:
On montre facilement que le théorème de Zermelo implique l'axiome du choix : comme pour les entiers naturels, si E est muni d'un bon ordre, le minimum pour celui-ci fournit une fonction de choix sur l'ensemble des parties non vides de E (second énoncé équivalent). De même le lemme de Zorn a également facilement pour conséquence l'axiome du choix.
Soit X une famille non vide d'ensembles non vides. Soit I l'ensemble des fonctions de choix f pour une sous-famille Y de X. L'ensemble I est non vide, car il est possible de définir sans l'axiome du choix une fonction de choix sur toute sous-famille finie de X. Cet ensemble est ordonné par le prolongement des applications. I est un ensemble inductif. Si le lemme de Zorn est vérifié, I admet un élément maximal, autrement dit une fonction de choix définie sur une sous-famille maximale Y de X. Si par l'absurde Y était différent de X, associer à un ensemble appartenant à X-Y un de ses éléments est toujours possible et permettrait de prolonger f à une sous-famille strictement plus grande, ce qui contredit la maximalité. Donc, Y=X et f est une fonction de choix pour X.
Les réciproques sont un peu plus délicates. On peut utiliser dans les deux cas assez naturellement la théorie des ordinaux, mais il est possible de démontrer le lemme de Zorn en travaillant directement sur la structure d'ordre de l'inclusion sur un ensemble de parties (c'est un ensemble inductif). Le théorème de Zermelo se déduit simplement du lemme de Zorn.