Description: Rule used to change bound variables, using implicit substitution. Version of cbval2vv with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 4-Feb-2005) Avoid ax-13 . (Revised by GG, 10-Jan-2024)