Description: Obsolete version of sb4vOLD as of 8-Jul-2023. Version of sb4OLD with a disjoint variable condition instead of a distinctor antecedent,
which does not require ax-13 . (Contributed by BJ, 23-Jun-2019)(Proof modification is discouraged.)(New usage is discouraged.)