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