This question is motivated by this and this. Can the following proposition be proved without Axiom of Choice?
Proposition: Let $k$ be a field. Let $A$ and $B$ be commutative algebras without zero-divisors which are finitely generated over $k$. Suppose that $A$ is a subring of $B$ and $B$ is integral over $A$. Let $P$ be a prime ideal of $A$. Then there exists a prime ideal $Q$ of $B$ such that $P = A \cap Q$.
First we show
Lemma If $A\to B$ is a finite homomorphism of rings with $A$ local and $B\ne 0$, then the maximal ideal $P$ of $A$ is the pre-image of a maximal ideal $Q$ of $B$.
Proof. By Nakayama's lemma, $PB\ne B$. The quotient $B/PB$ is a finite $k$-algebra (where $k$ is the field $A/P$) and is no zero. The set of proper ideals of $B/PB$ is non-empty and has an element of maximal $k$-vector space dimension. The latter is then a maximal ideal, hence equal to $Q/PB$ for some maximal ideal $Q$ of $B$ containing $P$. The pre-image $P'$ of $Q$ is maximal because $A/P'$ is contained in $B/Q$ and the later is finite over $A/P'$. So $P'=P$.
Now we prove your proposition. As $B$ is a finitely generated $A$-algebra, $B$ integral over $A$ implies that $B$ is finite over $A$. Hence $A_P\to A_P\otimes_A B$ is finite with $A_P\otimes_A B\ne 0$. By the above lemma, $PA_P$ is the pre-image of a maximal ideal of $A_P\otimes_A B$. The existence of $Q$ as desired follows from standard arguments on localizations.
This been said, I agree with the second part of Martin Brandenburg's comment.
Definition 1 Let $A$ be a commutative ring. Suppose $A$ has a unique maximal ideal. We say $A$ is a local ring in the usual sense.
Definition 2 Let $A$ be a commutative ring. Let $P$ be an ideal of $A$. Suppose that every element of $A - P$ is invertible. Then we say $A$ is a strictly local ring. Clearly $P$ is the unique maximal ideal of $A$. Hence $A$ is a local ring in the usual sense.
Note 1 It can be proved by using AC that a local ring in the usual sense is a strictly local ring. However, we are not supposed to use AC here.
Lemma 1 Let $A$ be commutative ring. Let $P$ be a prime ideal of $A$. Then $A_P$ is a strictly local ring.
Proof: Clear.
Definition 3 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Let $K$ be a field which contains $A$ as a subring. Let $x$ be an element of $K$. Let $x'$ be an element of some field containing $k$. We say $x'$ is a specialzation of $x$ over $P$ and we write $x \rightarrow x'$ over $P$, if there exists a homomorophism $\psi:A[x] \rightarrow (A/P)[x']$ extending the canonical homomorphism $A \rightarrow A/P$ and $\psi(x) = x'$. This is equivalent to that $\tilde{f}(x') = 0$ whenever $f(X) \in A[X]$ such that $f(x) = 0$,where $\tilde{f}(X) \in (A/P)[X]$ is the reduction of $f(X)$ mod $P$.
Lemma 2 Let $A$ be a strictly local domain. Let $\mathfrak{m}$ be the unique maximal ideal of $A$. Let $k = A/\mathfrak{m}$. Let $K$ be a field which contains A. Let $x \in K$. Suppose $x$ has no specializaion in any finite extension field of $k$ over $\mathfrak{m}$. Then $x$ is non-zero and $1/x \rightarrow 0$ over $\mathfrak{m}$.
Proof: Let $P$ = {$f \in A[X]$; $f(x) = 0$}. $P$ is an ideal of $A[X]$. Let $P'$ be the ideal of $k[X]$ generated by the set {$f(X)$ (mod $\mathfrak{m}$); $f(X) \in P$}. We claim that $P' = k[X]$. Suppose otherwise. Then $P'$ is generated by a polynomial $h(X) \in k[X]$, where $h(X)$ is not a non-zero constant. Hence $h(X)$ has a root $x'$ in a finite extension of k. Then $x \rightarrow x'$ over $\frak{m}$ This is a contradiction. Hence there exists $f(X) \in P$ such that $f(X)$ (mod $\mathfrak{m}$) is a non-zero constant. Let $f(X) = a_mX^m + ... + a_0$. Then $a_0 \in A - \mathfrak{m}$, $a_i \in \mathfrak{m}$ for $i > 0$. We assume that $m$ is minimal among the degrees of such polynomials. Let $y = 1/x$. Let $g(Y) = a_0Y^m + ... + a_m$ be a polynomial in $A[Y]$. Then $g(y) = 0$. Let $h(Y)$ be any polynomial in $A[Y]$ such that $h(y) = 0$. Since $A$ is a strict local ring, $a_0$ is invertible. Hence $Z^{m-1}h(Y) = g(Y)q(Y) + r(Y)$, where $q(Y), r(Y) \in A[Y]$ and deg $r \leq m - 1$. Substituting $Y$ by $y$ we get $r(y) = 0$. Taking the reductions mod $\mathfrak{m}$ of the both sides, we get $Y^{m-1}\tilde{h}(Y) = \tilde{a_0}Y^m\tilde{q}(Y) + \tilde{r}(Y)$. Hence $\tilde{h}(0) = \tilde{r}(Y)$. Since $\tilde{r}(Y)$ cannot be a non-zero constant by the minimality of $m$, $\tilde{h}(0) = 0$. Hence $z \rightarrow 0$ over $\mathfrak{m}$. QED
Note 2 The idea of the proof of Lemma 2 is borrowed from Weil's Foundations of algebraic geometry. According to him, the idea is due to Chevalley. See also Note 3 below.
Lemma 3 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. There exists a unique homomorphism $A_P \rightarrow k$ extending the canonical homomorphism $A \rightarrow A/P$.
Proof: Clear.
Lemma 4 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Let $K$ be a field which contains A as a subring. Let $x \in K$. Suppose $x$ has no specializaion in any finite extension of $k$ over $P$. Then $x$ is non-zero and $1/x \rightarrow 0$ over $P$.
Proof: Let $B = A_P$. By lemma 1, $B$ is a strictly local ring. Suppose $x \rightarrow x'$ over $PA_P$. By Lemma 3, $x \rightarrow x'$ over $P$. Hence $x$ has no specializaion in any finite extension of $k$ over $PA_P$. By Lemma 2, $1/x \rightarrow 0$ over $PA_P$. Hence, by Lemma 3, $1/x \rightarrow 0$ over $P$. QED
Note 3 Lemma 4 is a generalization of the one given in Weil's Foundations. He proved it when $A$ is a finitely generated domain over a field. Our Lemma 4 treats not only a case where $A$ and $A/P$ have equal characteristics but also a case of unequal ones.
Note 4 As van der Waerden and Weil showed, Lemma 4 has vast applications in algebraic geometry. For example, Hilbert Nullstellensatz can be proved by using it.
Lemma 5 Let $A$ be a domain. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Let $K$ be a field which contains $A$ as a subring. Let $x \in K$. Suppose $x$ is integral over $A$. Then there exist a finite extension $k'$ of $k$ and $x' \in k'$ such that $x \rightarrow x'$ over $P$.
Proof: Suppose there exists no such x'. By Lemma 4, there exists a homomorophism $\psi:A[1/x] \rightarrow k$ such that $\psi(1/x) = 0$ extending the canonical homomorphism $A \rightarrow A/P$. Let $y = 1/x$. Since $x$ is integral over $A$, $x^n + a_1x^{n-1} + ... + a_0 = 0$. Hence $1 + a_1y + ... + a_0y^n = 0$. Applying $\psi$, we get $1 = 0$. A contradiction. QED
Proposition Let $B$ be a domain. Let $A$ be a subring of $B$. Suppose $B$ is finitely generated as an $A$-module. Let $P$ be a prime ideal of $A$. Let $k$ be the field of fractions of $A/P$. Then there exist a finite extension $k'$ of $k$ and a homomorophism $\psi:B \rightarrow k'$ extending the canonical homomorphism $A \rightarrow A/P$.
Proof: This follows Immediately from Lemma 5.
Corollary Let $B$ be a domain. Let $A$ be a subring of $B$. Suppose $B$ is finitely generated as an $A$-module. Let $P$ be a prime ideal of $A$. Then there exists a prime ideal $Q$ of $B$ such that $P = A \cap Q$.
Proof: This follows Immediately from the proposition.
