Description: Rule used to change the bound variable in a universal quantifier with
implicit substitution. Deduction form. Version of cbvaldva with a
disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017)(Revised by Gino Giotto, 10-Jan-2024)
Reduce axiom usage, along an idea of Gino Giotto. (Revised by Wolf
Lammen, 10-Feb-2024)