The theory of Zermelo-Fraenkel sets with Hilbert $\varepsilon$-terms

In this paper we study the role of functioning axioms on the deductive power of the system obtained from the Zermelo–Fraenkel $\mathrm{ZF}$ system by the introduction of $\varepsilon$-terms with the possibility of using them as a scheme for the substitution axiom. It is proved that if the system has a founding axiom the introduction of $\varepsilon$-terms does not extend the class of $\mathrm{ZF}$ theorems, while if the founding axiom is absent, there is an extension of the $\mathrm{ZF}$ theorems.