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?

equivalence classesof certain well-founded graphs, as described in the nLab article on pure sets ncatlab.org/nlab/show/pure+set, so it looks like some set theory is being invoked there. But I'm supposing nothing more than that (compare the distinction between set and 'setoid': ncatlab.org/nlab/show/equivalence+relation). $\endgroup$