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?

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