Description: Weakened version of ax-7 1935,
with a dv condition on . This
should be the only proof referencing ax-7 1935,
and it should be
referenced only by its two weakened versions ax7v1 1937 and ax7v2 1938, from
which ax-7 1935 is then rederived as ax7 1943,
which shows that either ax7v 1936
or the conjunction of ax7v1 1937 and ax7v2 1938 is sufficient.
In ax7v 1936, it is still allowed to substitute the same
variable for
and , or the same variable for
and . Therefore,
ax7v 1936 "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 1941
and equid 1939 respectively. (Contributed by BJ,
7-Dec-2020.) Use ax7 1943
instead. (New usage is discouraged.) |