Description: A more general version of cbvrexf that has no distinct variable
restrictions. Changes bound variables using implicit substitution.
Usage of this theorem is discouraged because it depends on ax-13 .
(Contributed by Andrew Salmon, 13-Jul-2011)(Proof shortened by Mario
Carneiro, 7-Dec-2014)(New usage is discouraged.)