In light of Laurent Moret-Bailly's comment under Martin's answer, let us supplement that answer by showing how existence of prime ideals in finitely generated rings may be proven in ZF without a choice principle (not even the ultrafilter principle). In fact we will show that countable rings $R$ have prime ideals, using the weak König lemma.

(Recall the weak König lemma: if $T$ is an infinite subtree of the infinite binary tree $2^\ast$ [the nodes of $2^\ast$ are finite words in letters $0, 1$; the parent of any nonempty word is obtained by omitting its last letter], then $T$ has an infinite branch. This is easily proven in ZF; see e.g. here.)

Fix an enumeration $a_0, a_1, a_2, \ldots$ of elements of $R$. Build a tree $T$ whose nodes $w$ are labeled by ideals $P_w$ of $R$, by induction. $T_k$ will denote the set of nodes of length $k$, so $T_0$ consists of just the empty word $e$, which we label with the zero ideal. Assuming $T_{k-1}$ and the ideals $P_w$ for words $w \in T_{k-1}$ are given, define $T_k$ and the ideals there according to two cases; for this it is convenient to write $k = 2l + m$ where $m \in \{0, 1\}$ and $l$ is used to code a pair of natural numbers $(i, j)$ by the usual trick, viz. $l = \binom{i+j+1}{2} + j$.

Case $m = 0$: for each $w \in T_{k-1}$ such that $a_i a_j$ belongs to $P_w$, put $w0, w1$ in $T_k$, and define $P_{w0} := P_w + \langle a_i \rangle$, and $P_{w1} := P_w + \langle a_j \rangle$. For any other $w \in T_{k-1}$, put $w0$ in $T_k$, and define $P_{w0} = P_w$.

Case $m = 1$: for each $w \in T_{k-1}$ such that $1 \notin P_w$, put $w0$ in $T_k$, and define $P_{w0} := P_w$. If $1 \in P_w$, then put neither $w0$ nor $w1$ in $T_k$.

$T$ is infinite: it is easy to prove by induction that for each $k$ there is $w \in T_k$ such that $1 \notin P_w$. If $b$ is an infinite branch through $T$, then put $P = \bigcup_{w \in b} P_w$. Then $P$ is a proper ideal by the recipe of case $m=1$, and is prime by the recipe of case $m=0$.

In light of Laurent Moret-Bailly's comment under Martin's answer, let's add the simple argument that finitely generated rings have prime and even maximal ideals, without appealing to anything like a choice principle.

If $R$ is finitely generated (a quotient of some $\mathbb{Z}[x_1, \ldots, x_n]$), then it is countable. Enumerate its elements: $a_1, a_2, \ldots$. Form ideals $P_n$ by recursion: define $P_0 = \{0\}$, and given $P_{n-1}$, define $P_n = P_{n-1} + \langle a_n\rangle$ if this doesn't contain $1$, otherwise define $P_n = P_{n-1}$. The union of the $P_n$ is then a maximal ideal: it is proper because $1$ doesn't belong to any $P_n$. And if $a \notin P$ for some $a = a_n$, then $a_n \notin P_n$, meaning that $1 \in P_{n-1} + \langle a_n\rangle$ according to how $P_n$ was defined, and then $1 \in P + \langle a\rangle$. This proves maximality.

In light of Laurent Moret-Bailly's comment under Martin's answer, let us supplement that answer by showing how existence of prime ideals in finitely generated rings may be proven in ZF without a choice principle (not even the ultrafilter principle). In fact we will show that countable rings $R$ have prime ideals, using the weak König lemma.

(Recall the weak König lemma: if $T$ is an infinite subtree of the infinite binary tree $2^\ast$ [the nodes of $2^\ast$ are finite words in letters $0, 1$; the parent of any nonempty word is obtained by omitting its last letter], then $T$ has an infinite branch. This is easily proven in ZF; see e.g. here.)

Fix an enumeration $a_0, a_1, a_2, \ldots$ of elements of $R$. Build a tree $T$ whose nodes $w$ are labeled by ideals $P_w$ of $R$, by induction. $T_k$ will denote the set of nodes of length $k$, so $T_0$ consists of just the empty word $e$, which we label with the zero ideal. Assuming $T_{k-1}$ and the ideals $P_w$ for words $w \in T_{k-1}$ are given, define $T_k$ and the ideals there according to two cases; for this it is convenient to write $k = 2l + m$ where $m \in \{0, 1\}$ and $l$ is used to code a pair of natural numbers $(i, j)$ by the usual trick, viz. $l = \binom{i+j+1}{2} + j$.

Case $m = 0$: for each $w \in T_{k-1}$ such that $a_i a_j$ belongs to $P_w$, put $w0, w1$ in $T_k$, and define $P_{w0} := P_w + \langle a_i \rangle$, and $P_{w1} := P_w + \langle a_j \rangle$. For any other $w \in T_{k-1}$, put $w0$ in $T_k$, and define $P_{w0} = P_w$.

Case $m = 1$: for each $w \in T_{k-1}$ such that $1 \notin P_w$, put $w0$ in $T_k$, and define $P_{w0} := P_w$. If $1 \in P_w$, then put neither $w0$ nor $w1$ in $T_k$.

$T$ is infinite: it is easy to prove by induction that for each $k$ there is $w \in T_k$ such that $1 \notin P_w$. If $b$ is an infinite branch through $T$, then put $P = \bigcup_{w \in b} P_w$. Then $P$ is a proper ideal by the recipe of case $m=1$, and is prime by the recipe of case $m=0$.

In light of Laurent Moret-Bailly's comment under Martin's answer, let us supplement that answer by showing how existence of prime ideals in finitely generated rings may be proven in ZF without a choice principle (not even the ultrafilter principle). In fact we will show that countable rings $R$ have prime ideals, using the weak König lemma.

(Recall the weak König lemma: if $T$ is an infinite subtree of the infinite binary tree $2^\ast$ [the nodes of $2^\ast$ are finite words in letters $0, 1$; the parent of any nonempty word is obtained by omitting its last letter], then $T$ has an infinite branch. This is easily proven in ZF; see e.g. here.)

Fix an enumeration $a_0, a_1, a_2, \ldots$ of elements of $R$. Build a tree $T$ whose nodes $w$ are labeled by ideals $P_w$ of $R$, by induction. $T_k$ will denote the set of nodes of length $k$, so $T_0$ consists of just the empty word $e$, which we label with the zero ideal. Assuming $T_{k-1}$ and the ideals $P_w$ for words $w \in T_{k-1}$ are given, define $T_k$ and the ideals there according to two cases; for this it is convenient to write $k = 2l + m$ where $m \in \{0, 1\}$ and $l$ is used to code a pair of natural numbers $(i, j)$ by the usual trick, viz. $l = \binom{i+j+1}{2} + j$.

Case $m = 0$: for each $w \in T_{k-1}$ such that $a_i a_j$ belongs to $P_w$, put $w0, w1$ in $T_k$, and define $P_{w0} := P_w + \langle a_i \rangle$, and $P_{w1} := P_w + \langle a_j \rangle$. For any other $w \in T_{k-1}$, put $w0$ in $T_k$, and define $P_{w0} = P_w$.

Case $m = 1$: for each $w \in T_{k-1}$ such that $1 \notin P_w$, put $w0$ in $T_k$, and define $P_{w0} := P_w$. If $1 \in P_w$, then put neither $w0$ nor $w1$ in $T_k$.

$T$ is infinite: it is easy to prove by induction that for each $k$ there is $w \in T_k$ such that $1 \notin P_w$. If $b$ is an infinite branch through $T$, then put $P = \bigcup_{w \in b} P_w$. Then $P$ is a proper ideal by the recipe of case $m=1$, and is prime by the recipe of case $m=0$.