Description: Obsolete version of rmoeq1 as of 5-May-2023. Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017) (New usage is discouraged.) (Proof modification is discouraged.)