| Description: Axiom B7 of [Tarski] p. 75, which requires that x and y be
distinct. This trivial proof is intended merely to weaken Axiom ax-9 1654
by adding a distinct variable restriction. From here on, ax-9 1654
should
not be referenced directly by any other proof, so that Theorem ax9 1949
will show that we can recover ax-9 1654 from this weaker version if it were
an axiom (as it is in the case of Tarski).
Note: Introducing xy as a distinct variable group "out of
the
blue" with no apparent justification has puzzled some people, but
it is
perfectly sound. All we are doing is adding an additional redundant
requirement, no different from adding a redundant logical hypothesis,
that results in a weakening of the theorem. This means that any
future theorem that references ax9v 1655
must have a $d specified for the
two variables that get substituted for x and y. The $d does
not propagate "backwards" i.e. it does not impose a
requirement on
ax-9 1654.
When possible, use of this theorem rather than ax9 1949 is
preferred since
its derivation from axioms is much shorter. (Contributed by NM,
7-Aug-2015.) |
