Description: Bound-variable hypothesis builder for restricted quantification.
(Contributed by NM, 1-Sep-1999)(Revised by Mario Carneiro, 7-Oct-2016)(Proof shortened by Wolf Lammen, 30-Dec-2019) Add
disjoint variable condition to avoid ax-13 . See nfrexg for a less
restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)