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