Is material set theory conservative over structural set theory? Suppose a statement $\phi$ that doesn't use the global $\in$-relation or the global $=$-relation in an essential way is provable in some material set theory, say bounded Zermelo with choice. (So that the statement $\phi$ itself essentially is structural while, in theory, the intermediate steps in the proof of $\phi$ might be material, thus containing the global $\in$-relation or the global $=$-relation in an essential way!) Can it be proved that $\phi$ (or, rather, the translation of $\phi$ into the appropriate structural set theory) is nevertheless provable in some structural set theory, say ETCS, meaning that all the material intermediate steps can be eliminated?  (Note that since $\phi$ doesn't use the global $\in$-relation or the global $=$-relation in an essential way, such a translation should exist.)
Of course, in practice, most proofs are already structural. But who knows what crazy things could be done in theory by exploiting the global $\in$-relation?
I already know that ETCS and bounded Zermelo with choice are equiconsistent. Though related, it seems I'm asking for something stronger.
 A: This will obviously be highly dependent on the concrete theory you are considering. But overall the answer is yes.
The most general version of these results I'm aware of are in Mike Shulman's Comparing material and structural set theories. You'll find all the answer you want in this paper. But let me try to give you some pointers: I think the most relevant result here is lemma 9.1 which (roughly, see the paper for the details) says:
"Given $\mathbf{Set}$ ( a suitable pretopos, for eg. a model of ETCS) then the inclusion $\mathbb{S}\mathbb{V}(\mathbf{Set}) \to \mathbf{Set}$ is an equivalence if and only if every object of $\mathbf{Set}$ can be embedded into an extentional well founded graph"
where $\mathbb{V}$ denotes the construction described in Mike's paper that attach a material set theory to a structural theory and $\mathbb{S}$ takes a material set theory to its category of sets.
Any formula in $\phi$ in the language of a structural set theory is in particular a forumla in the 'language of categories' so is invariant by equivalence of categories. So, if the lemma applies, a formula $\phi$ is valid in $\mathbf{Set}$ if and only if it is valid in $\mathbb{S}\mathbb{V}(\mathbf{Set})$ that is exactly if the material translation of $\phi$ is valid in $\mathbb{V}(\mathbf{Set})$.
So if the material translation of $\phi$ is provable in the theory of $\mathbb{V}(\mathbf{Set})$ then it holds in $\mathbf{Set}$. If $\mathbf{Set}$ is a model of ETCS, then $\mathbb{V}(\mathbf{Set})$ satisfies Bounded Zermelo with choice ( and Mostowski principle and transitive closure, again, see mike's paper for the details). So that answer your question.
Note that, In the general case, the key condition is whether in $\mathbf{Set}$ every object can be embedded into an extentional well founded graph. Working with ETCS, or more generally if you have choice then this is really not a problem (e.g. put a well order on your set), but in more generality it might be problematic:
By construction material set theory (well founded and with transitive closure) always construct a set as a subset of an extentional well founded graph (its transitive closure with the $\in$ relation), so if your structural set theory cannot do this as well, this gives a counter-example to the question you are asking, as the existence of such an embedding is a meaningful structural statement.
Maybe there is a generalization of this construction that allows to get non well founded set theories that would go arround this problem, but I am not aware of this having been studied (?).
