Description: Rule used to change bound variables, using implicit substitution.
Version of cbvralf with a disjoint variable condition, which does not
require ax-10 , ax-13 . For a version not dependent on ax-11 and
ax-12, see cbvralvw . (Contributed by NM, 7-Mar-2004) Avoid
ax-10 , ax-13 . (Revised by Gino Giotto, 23-May-2024)