Description: Change the bound variable of a restricted at-most-one quantifier using
implicit substitution. Version of cbvrmo with a disjoint variable
condition, which does not require ax-10 , ax-13 . (Contributed by NM, 16-Jun-2017) Avoid ax-10 , ax-13 . (Revised by Gino Giotto, 23-May-2024)