**Description: **Weakened version of ax-7 1981,
with a dv condition on 𝑥, 𝑦. This
should be the only proof referencing ax-7 1981,
and it should be
referenced only by its two weakened versions ax7v1 1983 and ax7v2 1984, from
which ax-7 1981 is then rederived as ax7 1989,
which shows that either ax7v 1982
or the conjunction of ax7v1 1983 and ax7v2 1984 is sufficient.
In ax7v 1982, it is still allowed to substitute the same
variable for
𝑥 and 𝑧, or the same variable
for 𝑦 and 𝑧. Therefore,
ax7v 1982 "bundles" (a term coined by Raph
Levien) its "principal instance"
(𝑥
= 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) with 𝑥, 𝑦, 𝑧 distinct, and its
"degenerate instances" (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥)) and
(𝑥
= 𝑦 → (𝑥 = 𝑦 → 𝑦 = 𝑦)) with 𝑥, 𝑦 distinct. These
degenerate instances are for instance used in the proofs of equcomiv 1987
and equid 1985 respectively. (Contributed by BJ,
7-Dec-2020.) Use ax7 1989
instead. (New usage is discouraged.) |