Weakened version of [ax-9], with a disjoint variable condition on x , y. This should be the only proof referencing [ax-9], and it should be referenced only by its two weakened versions ax9v1 and ax9v2, from which [ax-9] is then rederived as ax9, which shows that either ax9v or the conjunction of ax9v1 and ax9v2 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax9 instead. (New usage is discouraged.)