The concept of elementary embedding is very important in the definition of several large cardinals ideas. The usual model-theoretic definition can not be expressed for some of these ideas within $\text{ZFC}$. There are various tricks to give satisfactory formalization of these ideas. My question is what are the usual ways of expressing concepts like elementary embedding?

For example, how would one express in $\text{ZFC}$ that a (class) function $j : M \rightarrow N$ is an elementary embedding between two (class) transitive structures. Of course, since $j$, $M$, and $N$ may be proper classes, these three will be expressed using their defining formulas; however, still the general satisfaction relation is not expressible. (However, I believe for any $n \in \omega$, the satisfaction relation for $\Sigma_n$ formulas of set theory is definable.)

Other troubling examples are expression that seem to quantify over elementary embeddings and inner models. For instance, in ZFC, it is provable that $\kappa$ is a measurable cardinal if and only if there is an inner model $M$ and an elementary embedding $j : V \rightarrow M$ with critical point $\kappa$. In the case of the measurable cardinal, perhaps the quantification could be replaced by quantifying over ultrafilter with certain properties since the $M$ can be taken to be Mostowski collapse of ultrapowers of $V$; however, is there a general way of expressing statements like the above that appear to quantify over elementary embeddings and inner models?

Also, one uses set elementary substructure of $V$ in $ZFC$. Just in ZFC, this is not possible since there are not even models of $ZFC$. However, often it suffices to consider substructures that are "sufficiently elementary". That is, it would be enought to have a set structure $X$ such that $X \prec_{\Sigma_n} V$. For any $n$, does such a set $\Sigma_n$-elementary substructure of $V$ always exists? This appears to be like the reflection principle for cumulative hierarchies (like $\{V_\alpha\}$ and $\{H_\alpha\}$); however, the form of the reflection principle I am familiar with from Kunen gives elementary substructures with respect to only finitely many formulas.

Thanks for any information that you can provide.