Description: Version of cbv3 with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof shortened by Wolf Lammen, 30-Aug-2021)