You may want to look at the [Tarski] reference at
http://us.metamath.org/mpeuni/mmset.html#bib showing how to formulate
predicate calculus without equality on p. 78:
Tarski, Alfred, "A Simplified Formalization of Predicate Logic with
Identity," Archiv für Mathematische Logik und
It seems like if one wants to define equality instead of "axiomizing" it,
it would be as
|- ( x = y <-> A. w ( w e. x <-> w e. y ) )
So I started doing a little digging to how much things would change if we
used that instead.
ax-7 |- ( x = y -> ( x = z -> y = z ) )
I think we can derive ax-7
