Description: Change bound variables in a class substitution. Interestingly, this
does not require any bound variable conditions on A . Usage of this
theorem is discouraged because it depends on ax-13 . Use the weaker
cbvcsbw when possible. (Contributed by Jeff Hankins, 13-Sep-2009)(Revised by Mario Carneiro, 11-Dec-2016)(New usage is discouraged.)