Description: Equality theorem for restricted unique existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004) (Revised by Andrew Salmon, 11-Jul-2011)