Why does this meta-theorem about relativization directly speak of the elements in the model rather than the constants available in the language? In Nik Weaver's book Forcing for Mathematicians, there is a so-called Proposition Scheme 6.1:

For any formula $φ$ in the language of set
theory with unquantified variables among $x_1, . . . , x_n$, the following statement is provable in ZFC.
Proposition Scheme 6.1. Let M and N be sets and suppose $f : M\cong N$ is an ∈-isomorphism. Then for all $a_1, . . . , a_n ∈ M$ we have $φ|_M(a_1, . . . , a_n) ↔ φ|_N(f(a_1), . . . , f(a_n))$.

The symbol $φ|_M $ above means the relativization to $M$.
I'm a bit confused by 'provable in ZFC': the elements $a_1, . . . , a_n ∈ M$ may not even be available in the language, i.e., there may be no constants whose interpretations cover the whole set $M$, how does that make sense?
Besides, I'm not so sure how the language of set theory can express the function $f$ from the meta-theory.
 A: The quantifiers in Proposition Scheme 6.1 are all ordinary quantifiers, not "meta-theoretic" quantifiers. The only "meta" quantifier here is over the formulas $\varphi$ (which is why the Proposition is a Scheme, not a single Proposition). To address your specific questions: (1) We don't need constants for the $a_i$, since they are quantified in the statement. (2) The function $f$ is not a function from the meta-theory, it is an ordinary set-theoretic function, i.e., a set of ordered pairs from $M\times N$.
For a fixed formula $\varphi$, let me partially translate the instance of Proposition Scheme 6.1 to the language of set theory:
$$\forall M\, \forall N\, \forall f\, (f\text{ is an $\in$-isomorphism $M\to N$})\rightarrow (\forall a_1,\dots,a_n\, (\bigwedge_{i<n}a_i\in M)\rightarrow (\varphi|_M(a_1,\dots,a_n)\leftrightarrow \varphi|_N(f(a_1),\dots,f(a_n))).$$
I hope it's clear that this is a sentence in the language of set theory (once you expand what it means for $f$ to be an $\in$-isomorphism, and once you syntactically transform $\varphi$ to $\varphi|_M$ and $\varphi|_N$), so it makes sense to assert that it's provable in ZFC.
