What axiom of ZFC implies that "sets have no repeated elements"?

Question

For example, the axiom of pairing says:

Let $a$ be a set.

Let $b$ be a set.

If follows that the set $\{a,b\}$ exists.

This can be used to prove the existence of singletons, for instance, by setting $b := a$ (in the previous statement). Namely, the axiom of pairing implies the following:

Let $a$ be a set.

If follows that the set $\{a\}$ exists.

---

This got me thinking. What ZFC axiom implies that, for any set $a$, the set $\{a,a\}$ equals the set $\{a\}$? Equivalently, what axiom of ZFC implies that the sets of ZFC don't behave like multisets? (I suspect it's extensionality, but I couldn't argue why. So, if it is extensionality, then I'm gonna need some convincing...)

Answer 1

The axiom of extensionality is the statement:

Axiom of extensionality.
Let $A$ be a set.
Let $B$ be a set.
IF for every set $x$ $($ $x$ is in $A$ $ $ $ $ IFF $ $ $ $ $x$ is in $B$ $)$,
THEN $A$ equals $B$.

We can use this to prove the "no repeated elements" property by setting $A := \{a,a\}$ and $B := \{a\}$ in the axiom of extensionality. So,

Theorem. The set {a,a} equals the set $\{a\}$.
Proof. Since $\{a,a\}$ and $\{a\}$ are sets, they satisfy the hypotheses of the axiom of extensionality. So, they satisfy the conclusion.
This means that the sets $\{a,a\}$ and $\{a\}$ satisfy the implication:

IF for every set $x$ $($ $x$ is in $\{a,a\}$ $ $ $ $ IFF $ $ $ $ $x$ is in $\{a\}$ $)$,
THEN $\{a,a\}$ equals $\{a\}$.

So, if we can prove the antecedent

$(*)$ for every set $x$ $($ $x$ is in $\{a,a\}$ $ $ $ $ IFF $ $ $ $ $x$ is in $\{a\}$ $)$,

then, by modus ponens, it'll follow that

$\{a,a\}$ equals $\{a\}$,

as desired.

We prove $(*)$ by verifying it for every element of $\{a,a\}$ and $\{a\}$.
The key observation is that: $a$ is in $\{a,a\}$ and $a$ is in $\{a\}$.

0. The 1st element of $\{a,a\}$ is $a$. By the truth table of IFF, it holds that: $a$ is in $\{a,a\}$ $ $ IFF $ $ $a$ is in $\{a\}$.
1. The 2nd element of $\{a,a\}$ is $a$. By the truth table of IFF, it holds that: $a$ is in $\{a,a\}$ $ $ IFF $ $ $a$ is in $\{a\}$.
2. The 1st element of $\{a\}$ is $a$. By the truth table of IFF, it holds that: $a$ is in $\{a,a\}$ $ $ IFF $ $ $a$ is in $\{a\}$.
3. There are no other elements in $\{a,a\}$ or $\{a\}$.

This proves that: for every set $x$ $($ $x$ is in $\{a,a\}$ $ $ $ $ IFF $ $ $ $ $x$ is in $\{a\}$ $)$.

This proves that: $\{a,a\}$ equals $\{a\}$.

A similar argument proves that: $\{a,a,a\}$ equals $\{a\}$, and so on.

To extend this result to every finite number of $a$'s probably requires induction, which probably requires the axiom of infinity.

Answer 2

It is indeed the extensionality axiom that is at play here.

We have

$$\forall x (x \in A \iff x \in B)$$ where $A = \{a,a\}$ and $B=\{a\}$ as for both sets $A$ and $B$, $x$ belongs to one of those set if and only if $x=a$.

Therefore $A=B$ by entensionality.