|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 1449). Axiom scheme C8'
in [Megill] p. 448 (p. 16 of the preprint).
Also appears as Axiom C7 of
[Monk2] p. 105.
Axioms ax-8 1301 through ax-16 1540 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 1540 and ax-17 1320 are still valid even when x, y, and
z 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 1540 and ax-17 1320 only. (Contributed by