These logic/ZFC/model theory arguments seem out of proportion to the task at hand. Let $k$ be a field and $A$ a finitely generated $k$-algebra which is a field. We want to prove that $A$ is $k$-finite (i.e., finite-dimensional as a $k$-vector space). Pick an extension field $k'/k$ (e.g., algebraic closure of a massive transcendental extension, or whatever), and we want to show that if the result is known in general over $k'$ then it holds over $k$. We just need some very basic commutative algebra, as follows.
Proof: Consider the maximal reduced quotient $$A' = (A \otimes_k k') _{\rm{red}};$$ this is a reduced finitely generated $k'$-algebra and integral over the field $A$, so its minimal primes $\mathfrak{p}$ are also maximal and its quotient by any such $\mathfrak{p}$ is a field that is finitely generated as a $k'$-algebra. By the assumed Nullstellensatz over $k'$, $A'/\mathfrak{p}$ is $k'$-finite. But $A'$ injects into the product of these finitely many quotients $A'/\mathfrak{p}$, so $A'$ is itself $k'$-finite. The nilradical $J$ of $A \otimes_k k'$ satisfies $J^n = 0$ for some large $n$, and each $J^i/J^{i+1}$ is a finitely generated $A'$-module, hence is $k'$-finite. Thus, $A \otimes_k k'$ is $k'$-finite, so $A$ is $k$-finite. QED
I think the main point is the principle of proving a result over a field by reduction to the case of an extension field with more properties (e.g., algebraically closed). That is very useful.