Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017) (Proof shortened by Wolf Lammen, 28-Feb-2018)