The axiom "There exists some nonprincipalultrafilter." is discussed in Horst Herrlich, "The Axiom of Choice" as WUF(?) and in Rubin and Rubin "Equivalents of the Axiom of Choice, II." under [206]. The latter is kind of the standard ressource for these kinds of questions.

Here are papers providing proofs:

For 1:

MR0480028 (58 #227) Pincus, David ; Solovay, Robert M. Definability of measures and ultrafilters. J. Symbolic Logic 42 (1977), no. 2, 179--190.

For 2:

MR0480027 (58 #226) Pincus, David . Adding dependent choice to the prime ideal theorem. Logic Colloquium 76 (Oxford, 1976), pp. 547--565. Studies in Logic and Found. Math., Vol. 87, North-Holland, Amsterdam, 1977.

The axiom "There exists some nonprincipalultrafilter." is discussed in Horst Herrlich, "The Axiom of Choice" as WUF(?) and in Rubin and Rubin "Equivalents of the Axiom of Choice, II." under [206]. The latter is kind of the standard ressource for these kinds of questions.

Here are papers providing proofs:

For 1:

MR0480028 (58 #227) Pincus, David ; Solovay, Robert M. Definability of measures and ultrafilters. J. Symbolic Logic 42 (1977), no. 2, 179--190. JSTOR, doi: 10.2307/2272118

For 2:

MR0480027 (58 #226) Pincus, David . Adding dependent choice to the prime ideal theorem. Logic Colloquium 76 (Oxford, 1976), pp. 547--565. Studies in Logic and Found. Math., Vol. 87, North-Holland, Amsterdam, 1977. doi: 10.1016/S0049-237X(09)70445-8

The axiom "There exists some nonprincipalultrafilter." is discussed in Horst Herrlich, "The Axiom of Choice" as WUF(?) and in Rubin and Rubin "Equivalence of the Axiom of Choice, II." under [206]. The latter is kind of the standard ressource for these kinds of questions.

Here are papers providing proofs:

For 1:

MR0480028 (58 #227) Pincus, David ; Solovay, Robert M. Definability of measures and ultrafilters. J. Symbolic Logic 42 (1977), no. 2, 179--190.

For 2:

MR0480027 (58 #226) Pincus, David . Adding dependent choice to the prime ideal theorem. Logic Colloquium 76 (Oxford, 1976), pp. 547--565. Studies in Logic and Found. Math., Vol. 87, North-Holland, Amsterdam, 1977.

The axiom "There exists some nonprincipalultrafilter." is discussed in Horst Herrlich, "The Axiom of Choice" as WUF(?) and in Rubin and Rubin "Equivalents of the Axiom of Choice, II." under [206]. The latter is kind of the standard ressource for these kinds of questions.

Here are papers providing proofs:

For 1:

MR0480028 (58 #227) Pincus, David ; Solovay, Robert M. Definability of measures and ultrafilters. J. Symbolic Logic 42 (1977), no. 2, 179--190.

For 2:

MR0480027 (58 #226) Pincus, David . Adding dependent choice to the prime ideal theorem. Logic Colloquium 76 (Oxford, 1976), pp. 547--565. Studies in Logic and Found. Math., Vol. 87, North-Holland, Amsterdam, 1977.