Description: Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on ax-13 . Use the
weaker cbvmow , cbvmovw when possible. (Contributed by NM, 9-Mar-1995)(Revised by Andrew Salmon, 8-Jun-2011)(Proof shortened by Wolf Lammen, 4-Jan-2023)(New usage is discouraged.)