Description: Rule used to change bound variables, using implicit substitution.
Version of cbvex2vv with more disjoint variable conditions, which
requires fewer axioms . (Contributed by NM, 26-Jul-1995) Avoid
ax-13 . (Revised by Gino Giotto, 10-Jan-2024)