Version of axc11r with a disjoint variable condition on \( x \) and \( y \), which is provable, on top of { [ax-1] -- [ax-7] }, from ax12v (contrary to axc11 which seems to require the full [ax-12] and [ax-13], and to axc11r which seems to require the full [ax-12] ). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)