Version of axc11 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] ). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)