Description: Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on ax-13 . Check
out cbvexvw , cbvexv1 for weaker versions requiring fewer axioms.
(Contributed by NM, 21-Jun-1993)(New usage is discouraged.)