Description: Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on ax-13 . See
cbv2w with disjoint variable conditions, not depending on ax-13 .
(Contributed by NM, 5-Aug-1993)(Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style, avoid ax-10 .
(Revised by Wolf Lammen, 10-Sep-2023)(New usage is discouraged.)