Description: Obsolete as of 30-Jul-2023. Use sb6 instead. Version of sb2 with a
disjoint variable condition, which does not require ax-13 .
(Contributed by BJ, 31-May-2019) Revise df-sb . (Revised by Steven
Nguyen, 8-Jul-2023)(Proof modification is discouraged.)(New usage is discouraged.)