|Description: Axiom of Equality. One
of the equality and substitution axioms of
predicate calculus with equality. This is similar to, but not quite, a
transitive law for equality (proved later as equtr 1826). Axiom scheme C8'
in [Megill] p. 448 (p. 16 of the
preprint). Also appears as Axiom C7 of
[Monk2] p. 105.
This is our first use of the equality symbol, invented in 1527 by Robert
Recorde. He chose a pair of parallel lines of the same length because
"noe .2. thynges, can be moare equalle."
Axioms ax-8 1623 through ax-16 1926 are the axioms having to do with equality,
substitution, and logical properties of our binary predicate (which
later in set theory will mean "is a member of"). Note that all
except ax-16 1926 and ax-17 1628 are still valid even when , , and
are replaced with
the same variable because they do not have any
distinct variable (Metamath's $d) restrictions. Distinct variable
restrictions are required for ax-16 1926 and ax-17 1628 only. (Contributed by