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) (Revised by Gino Giotto, 10-Jan-2024)