|Description: Axiom of Equality. One
of the equality and substitution axioms for a
non-logical predicate in our predicate calculus with equality. It
substitutes equal variables into the left-hand side of the binary
predicate. Axiom scheme C12' in [Megill]
p. 448 (p. 16 of the preprint).
It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77.
"Non-logical" means that the predicate is not a primitive of
calculus proper but instead is an extension to it. "Binary"
the predicate has two arguments. In a system of predicate calculus with
equality, like ours, equality is not usually considered to be a
non-logical predicate. In systems of predicate calculus without equality,
it typically would be. (Contributed by NM,