Description: Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim . Usage of this
theorem is discouraged because it depends on ax-13 . See cbvaldw for a version with x , y disjoint, not depending on ax-13 .
(Contributed by NM, 2-Jan-2002)(Revised by Mario Carneiro, 6-Oct-2016)(Revised by Wolf Lammen, 13-May-2018)(New usage is discouraged.)