Description: Obsolete version of equsb1v as of 19-Jun-2023. (Contributed by BJ, 11-Sep-2019) Remove dependencies on axioms. (Revised by Wolf Lammen, 30-May-2023)(Proof shortened by Steven Nguyen, 31-May-2023)(New usage is discouraged.)(Proof modification is discouraged.)