**Description: **Axiom B7 of [Tarski] p. 75, which requires that and be
distinct. This trivial proof is intended merely to weaken axiom ax-9 1635
by adding a distinct variable restriction. From here on, ax-9 1635
should
not be referenced directly by any other proof, so that theorem ax9 1889
will show that we can recover ax-9 1635 from this weaker version if it were
an axiom (as it is in the case of Tarski).
Note: Introducing 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 1636
must have a $d specified for the
two variables that get substituted for and . The $d does
not propagate "backwards" i.e. it does not impose a
requirement on
ax-9 1635.
When possible, use of this theorem rather than ax9 1889 is
preferred since
its derivation from axioms is much shorter. (Contributed by NM,
7-Aug-2015.) |