Description: Restricted existential uniqueness of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024)