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