How to get an element from an existential proposition in Type theory proof assistant (Lean prover)
The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (only $\in$ relation). But even just stating the axioms of set theory without any constants and operation symbols is pretty haunting, see this gist of mine.

If you want a workable set theory you will have to rephrase your axioms so that they are not existential statements but rather operations. For example, define a union : Set → Set → Set operation and an axiom which states that u ε union X Y ↔ u ε X ∨ u ε Y. Formally, set theory does not have these operations, but every single development of set theory relies on the meta-theorem which says that introducing such constants is conservative (they can be eliminated). Also for the inductive set, introduce a constant S : Set and the axiom inductiveset S.

As a general advice, when formalizing mathematics in a proof assistants, one has to be quite flexible about organization of material. Traditional organization is good for teaching and writing textbooks, and so it may not align well with the demands of formalization.

For example, it looks to me at first sight that you would benefit by formalizing not only sets, but also classes. The class comprehension notation $\{ x \mid \phi(x) \}$ is very expressive and convenient, and easily formalized in terms of propositional functions on $\mathsf{Set}$. With it, you can define many operations on classes and then state that they are sets in terms of axioms. For example, rather than axiomatizing a union operation we just define union X Y to be the class {u | u ε X ∨ u ε Y} and then state that this class is a set. I suppose you could look at Von Neumann–Bernays–Gödel set theory.