Weakened version of [ax-7], with a disjoint variable condition on x , y. This should be the only proof referencing [ax-7], and it should be referenced only by its two weakened versions ax7v1 and ax7v2, from which [ax-7] is then rederived as ax7, which shows that either ax7v or the conjunction of ax7v1 and ax7v2 is sufficient.

In ax7v, it is still allowed to substitute the same variable for \( x' \) and \( z' \), or the same variable for \( y' \) and \( z' \). Therefore, ax7v "bundles" (a term coined by Raph Levien) its "principal instance" \( x' = y' \rightarrow x' = z' \rightarrow y' = z' \) with x , y , z distinct, and its "degenerate instances" \( x' = y' \rightarrow x' = x' \rightarrow y' = x' \) and \( x' = y' \rightarrow x' = y' \rightarrow y' = y' \) with x , y distinct. These degenerate instances are for instance used in the proofs of equcomiv and equid respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 instead. (New usage is discouraged.)