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.