Description: Equivalence of two versions of the Axiom of Choice ax-ac . The proof uses the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by Mario Carneiro, 17-May-2015)