Since you asked for a proof, let me complement Chris Phan's answer by outlining a proof which that relies only on the Compactness Theorem for propositional logic, which is yet another equivalent to the Ultrafilter Theorem over ZF.
Let A be a commutative ring and let x ∉ Nil(A). To each element a ∈ A associate a propositional variable pa and let T be the theory whose axioms are
- p0, ¬p1, ¬px, ¬px2, ¬px3,...
- pa ∧ pb → pa+b for all a, b ∈ A.
- pa → pab for all a, b ∈ A.
- pab → pa ∨ pb for all a, b ∈ A.
Models of T correspond precisely to prime ideals that do not contain x. Indeed, if I P is such an ideal, then setting pa to be true iff a ∈ I P satisfies all of the above axioms, and conversely. So it suffices to show that T has a model.
Since xn ≠ 0 for all n, one can verify using ideals over finitely generated subrings of A that the theory T is finitely consistent, i.e. any finite subset of T has a model. (What I just swept under the rug here is a constructive proof of the theorem for quotients of Z[v1,...,vn].) The Compactness Theorem for propositional logic then ensures that T has a model.