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.
