Which kind of foundation are mathematicians using when proving metatheorems? Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. For every two objects/sets $a,b$ one can ask whether $a=b$ or not. Also, one can always ask whether $a\in b$ is true or not. So $\in$ is a global element relation.
As an alternative foundation for set theory, Shulman proposed SEAR. It is a structural set theory. That is, elements have no internal structure, i.e. are just "abstract dots". One has a type declaration $a\colon A$ for saying that $a$ is an element of $A$. But this can't be negated, so $\colon$ is no relation. But if $A$ is a set (should I say "abstract set" for emphasizing the point that I mean "set in a structural set theory"?), then one has a local element relation $\in_A$: for each element $a$ in $A$ and each subset $B$ of $A$ (= function $A\to 2:=\{0,1\}$), the statement $a\in_A B:\iff B(a)=1$ is either true or false.
On the SEAR-page I linked to above, there is a proof (due to Shulman I guess) showing that SEAR and ZF are basically equivalent: from a model of ZF one can construct a model of SEAR and vice versa. This is a meta theorem. But in which foundation does the proof of such a meta theorem take place? Is this meta foundation a structural or a material set theory?
 A: Your question is much more specific than your title suggests.  As to the question itself, my answer is that it doesn't matter.  The proof is given in mathematics, not in any formal system.  A foundation for mathematics, in order to count as a foundation of mathematics, must be able to formalize most ordinary mathematical arguments.  Thus, any foundation for mathematics could be used to formalize such a metatheorem.
With that said, some people care about whether metatheorems of this sort can be formalized in very weak theories.  There's nothing wrong with that, but it's not something I spend my time thinking about, and in particular I didn't think about it when writing the proof you refer to.  The closest I came was noting that instead of a "construction of a model" the proof can equivalently be regarded as giving a translation of first-order formulas.  If you're interested in this sort of question, then Nik's answer seems reasonable to me, but I'm not familiar with the details of how this sort of thing goes.
A: One direction could go like this. Let ${\rm ZFC}^+$ be the theory in the language of set theory augmented by a constant symbol ${\bf M}$ with the axioms
$\bullet$ every axiom of ${\rm ZFC}$
$\bullet$ "${\bf M}$ is countable and transitive"
$\bullet$ the relativization of every axiom of ${\rm ZFC}$ to ${\bf M}$.
Then one can prove ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm ZFC}^+)$ in Peano arithmetic, and based on the page you linked, it looks like one can straightforwardly prove the consistency of any finite fragment of ${\rm SEAR}$ in ${\rm ZFC}^+$. Thus one can prove ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm SEAR})$ in Peano arithmetic. (If ${\rm SEAR}$ were not consistent then some finite fragment ${\rm SEAR}_0$ would be inconsistent, and this fact would be verifiable in ${\rm ZFC}^+$, so that ${\rm ZFC}^+$ would prove both ${\rm Con}({\rm SEAR}_0)$ and $\neg{\rm Con}({\rm SEAR}_0)$ and hence be inconsistent.) For details see Chapter 7 of my book.
I imagine a similar argument would work in the reverse direction to prove ${\rm Con}({\rm SEAR}) \Rightarrow {\rm Con}({\rm ZFC})$ in Peano arithmetic, but I'm not familiar with ${\rm SEAR}$ so I can't say that for sure.
