Description: Obsolete version of rexeq as of 5-May-2023. Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.) (Proof modification is discouraged.)