TITLE: Axiom of pairing for equivalent sets
QUESTION [3 upvotes]: A teacher of logic in my university gave us the following definition of axiom of pairing which differs from Wikipedia's one:
$\forall x\forall y(\lnot x=y \to \exists p(x \in p\ \&\ y \in p\ \&\ \forall z(z \in p \to (z = x \lor z = y))))$.
At the exam he asked me why do we need the $\lnot x=y$ condition and I didn't manage to find any reason. He asked me, if we can get the set $\{ a, b\}$ where $a = b$ and I gave him a way to do that with some usages of other Zermelo–Fraenkel axioms. Then he asked whether $\{ a, a\}$ equals to $\{ a \}$. I said "yes, judging by the definition of set equality". He asked: "So what's the deal with the $\lnot x=y$ condition then?" and I was back to square one. So now I'm interested what's really the deal with it?
P.S. I passed the exam

REPLY [3 votes]: The $\neg x=y$ condition is completely unnecessary, and in fact is usually not included in the presentation of the ZF axioms (I have actually personally never seen it included).  As you have observed, in the presence of the other ZF axioms, it does not make any difference whether you include $\neg x=y$.  If you have no other axioms, including $\neg x=y$ gives you a weaker axiom, but I don't know of any context in which it is desirable to have this weaker axiom instead of the stronger version without it.
In sum, the standard answer to your teacher's question is "we don't".  If he has some other answer in mind, then it is something peculiar to his tastes or to something unusual you did in your course.
{"set_name": "stack_exchange", "score": 3, "question_id": 2240659}