This question already has an answer here:

I think this is a definition of = because it explains the meaning of the new symbol =. However, I wonder why the set theory thinks this as an axiom rather than a definition.


marked as duplicate by José Carlos Santos, Asaf Karagila logic Jan 21 at 9:41

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.


See Axiom of extensionality.

There are two possibilities :

(i) the underlying logic is predicate calculus with equality.

In this case, the symbol $=$ is already defined by the equality axiom and Extensionality is needed only to legislate the "interaction" with $\in$ :

$∀x∀y∀z [(z ∈ x \leftrightarrow z ∈ y) \to x = y]$.

(ii) the underlying logic is predicate calculus without equality.

In this case you are right : we need a specific definition for equality :

$a=b =_{def} \forall x [x \in a \leftrightarrow x \in b]$

and a different version of Extensionality :

$\forall z \forall x \forall y [x = y \to (x \in z \to y \in z)]$.

From them we can derive the usual properties of equality.

  • $\begingroup$ +1 Very enlightening. $\endgroup$ – drhab Jan 21 at 9:22
  • $\begingroup$ Thank you very much! Can you tell me exactly what the (slightly different) version of Extensionality is? $\endgroup$ – amoogae Jan 21 at 9:36
  • $\begingroup$ I just read your edited answer. Thank you so much! $\endgroup$ – amoogae Jan 21 at 11:01

Not the answer you're looking for? Browse other questions tagged or ask your own question.