Description: Change the bound variable of a class substitution using implicit
substitution. Version of cbvsbcv with a disjoint variable condition,
which does not require ax-13 . (Contributed by NM, 30-Sep-2008)
Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024)