  With a bit of work, it can be shown that (1) defines a unique set in standard set theory ZFC.  (1) is more of a characterization than a textbook definition, however.  In other words, if one were presented with (1) as a putative definition, then the first step in understanding it  would be to “straighten out” the circularity by providing a different definition D of a set, then to check that every set satisfying D satisfies the property defining HF, and vice-versa.