Description: Similar to Lemma 24 of Monk2 p. 114, except the quantification of the
antecedent is restricted. Derived automatically from hbra2VD .
Contributed by Alan Sare 31-Dec-2011. Usage of this theorem is
discouraged because it depends on ax-13 . Use the weaker nfra2w when possible. (Contributed by NM, 31-Dec-2011)(New usage is discouraged.)