Description: Obsolete version of equsb1v as of 22-Jul-2023. Version of equsb1 with a disjoint variable condition, which neither requires ax-12 nor
ax-13 . (Contributed by BJ, 11-Sep-2019) Remove dependencies on
axioms. (Revised by Wolf Lammen, 30-May-2023)(Proof shortened by Steven Nguyen, 19-Jun-2023) Revise df-sb . (Revised by Steven
Nguyen, 11-Jul-2023)(Proof modification is discouraged.)(New usage is discouraged.)