Description: Obsolete version of sb2 as of 8-Jul-2023. Version of sb2 with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 31-May-2019) (New usage is discouraged.) (Proof modification is discouraged.)