There is something about extensionality axiom which makes debatable its use in any theory, not only in an algebraic one -- this law looks more like a definition than a statement when written like this:
$\forall z (z \in x \leftrightarrow z \in y) \leftrightarrow x = y$
It might be recommendable to use a form of this law which (only) looks like a weaker statement like this:
$\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y$,
but since the inverse is deducible, for the purposes of this question, I used the first form.
The extensionality axiom never caused me logical discomfort of this kind when I dealt with regular set theories, but now I am intested in algebraization of set theory and I got a feeling that this statement will create many problems in algebraization. This is why I asked the question about correctness of extensionality axiom specifically in an algebraic set theory. However, I started now having some logical discomfort with its presence in formalized regular set theories (informally everything that is understood is acceptable). Here is another question associated with those asked in title:
Is it acceptible to use hidden or obvious definitions in a formal theory, and how one can detect which statements are hidden definitions?
A question about a problem which does not distract with superfluous information has more chances to get an answer. This is why I referred in my question to a theory with only this axiom and the axioms of equality (identity).
This theory showcases a certain kind of logical difficulty and I would like in my communication with students to reference this difficulty by using a name. That is why I asked weather the name ``extensionality theory'' sounds appropriate (i.e. it does not refer to another phenomenon, or something like this).
ADDITION: The extensionality axiom contains the symbol "$\in$" of a relation and it cannot be used as it is in an algbraic set theory, but my question implied that this symbol is expressed through adjunction operation in the algebraic theory. The adjunction operation "$\rhd$" is defined like this $x \rhd y \rightleftharpoons x \cup \{ y\}$. Therefore, $x \in y \rightleftharpoons (y \rhd x = y)$. Thus, one can substitute the left hand expression with the right hand expression in the extensionality axiom, and this will contain no symbol of relation in its new form.
