show/hide this revision's text 2 added details

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.
show/hide this revision's text 1

Since you asked for a proof, let me complement Chris Phan's answer by outlining a proof which relies only on the Compactness Theorem for propositional logic, which is 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 is such an ideal, then setting pa to be true iff a ∈ I 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. The Compactness Theorem for propositional logic then ensures that T has a model.