Description: Bound-variable hypothesis builder for restricted unique existence.
Version of nfreu with a disjoint variable condition, which does not
require ax-13 . (Contributed by NM, 30-Oct-2010) Avoid ax-13 .
(Revised by Gino Giotto, 10-Jan-2024) Avoid ax-9 , ax-ext .
(Revised by Wolf Lammen, 21-Nov-2024)