# Why is the “axiom of extension” an axiom? [duplicate]

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 StackExchange.ready(function() { if (StackExchange.options.isMobile) return; $('.dupe-hammer-message-hover:not(.hover-bound)').each(function() { var$hover = $(this).addClass('hover-bound'),$msg = $hover.siblings('.dupe-hammer-message');$hover.hover( function() { $hover.showInfoMessage('', { messageElement:$msg.clone().show(), transient: false, position: { my: 'bottom left', at: 'top center', offsetTop: -7 }, dismissable: false, relativeToBody: true }); }, function() { StackExchange.helpers.removeMessages(); } ); }); }); Jan 21 at 9:41

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.

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