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