Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfrbi for equivalence version. (Contributed by NM, 21-Aug-2007)