Description: Equality theorem for restricted existential quantifier, with
bound-variable hypotheses instead of distinct variable restrictions.
See rexeq for a version based on fewer axioms. (Contributed by NM, 9-Oct-2003)(Revised by Andrew Salmon, 11-Jul-2011)(Proof shortened by Wolf Lammen, 9-Mar-2025)