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](http://www.ams.org/mathscinet-getitem?mr=0480028) (58 #227)  Pincus, David ;  Solovay, Robert M.  Definability of measures and ultrafilters.
J. Symbolic Logic  42  (1977),  no. 2, 179--190. [JSTOR](http://www.jstor.org/stable/2272118), doi: [10.2307/2272118](https://doi.org/10.2307/2272118)

For 2:

[MR0480027](http://www.ams.org/mathscinet-getitem?mr=0480027) (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](https://doi.org/10.1016/S0049-237X(09)70445-8)