Why include equality in FOL for ZFC?

Question

What are the pros and cons of working with first-order logic with equality for constructing ZFC, when all you have to do is make '$x=y$' a shorthand for: $$'\forall z [z \in x \Leftrightarrow z \in y] \land \forall w [x \in w \Leftrightarrow y \in w]'$$

Answer 1

There are two "flavours" of first-order logic: with and without equality.

In the first case (with), the equality symbol is considered a logical symbol, i.e. we cannot "interpret" it in different ways according to the context (like the conncetive and the quantifiers).

In the second one (without) the equality symbol is considered a "mathematical" symbol, like $+$ for f-o arithmetic, and thus (in principle) may be interpreted in different ways according to the context.

---

If we chose to develop set theory in f-o language without equality, we have to expand the "basic" language with the new (binary) predicate symbol $=$ defined by:

$(x=y) ↔ ∀z(z∈x ↔ z∈y)$.