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.