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 (?).

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 (?).

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 as far as I know this hasn't been developed (?).

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 (?).