Description: Weakened version of ax-7 1965,
with a disjoint variable condition on
𝑥,
𝑦. This should be
the only proof referencing ax-7 1965, and it
should be referenced only by its two weakened versions ax7v1 1967 and
ax7v2 1968, from which ax-7 1965
is then rederived as ax7 1973, which shows
that either ax7v 1966 or the conjunction of ax7v1 1967 and ax7v2 1968 is
sufficient.
In ax7v 1966, it is still allowed to substitute the same
variable for
𝑥 and 𝑧, or the same variable
for 𝑦 and 𝑧. Therefore,
ax7v 1966 "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 1971
and equid 1969 respectively. (Contributed by BJ,
7-Dec-2020.) Use ax7 1973
instead. (New usage is discouraged.) |