Description: Similar to Lemma 24 of Monk2 p. 114, except the quantification of the
antecedent is restricted. Derived automatically from hbra2VD .
Version of nfra2 with a disjoint variable condition, which does not
require ax-13 . (Contributed by Alan Sare, 31-Dec-2011)(Revised by Gino Giotto, 10-Jan-2024)