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 GG, 10-Jan-2024)