Description: Axiom of Choice (first form) of Enderton p. 49 corresponds to our
Axiom of Choice (in the form of ac3 ). The proof does not make use of
AC, but the Axiom of Regularity is used (by applying dfac2b ).
(Contributed by NM, 5-Apr-2004)(Revised by Mario Carneiro, 26-Jun-2015)(Revised by AV, 16-Jun-2022)