The English statement does not make sense. In first-order logic, there are two syntactic categories: terms and formulas. Semantically, terms range over objects and formulas range over properties of those objects. One can say that an object satisfies some property but not that a property satisfies another property (for this you need second-order logic). Therefore, H(y,x) cannot satisfy G(x). I think you mean that y such that H(y,x) satisfies G (and not G(x)). Also, the universal quantifier over x has to extend over the whole formula because otherwise x in H(y,x) is unbound. So, I think the English sentence should say,

If F(x) is not true then no y such that H(y,x) satisfies G

and its translation is

∀x (¬F(x) ⇒ ¬∃y (H(y,x) ˄ G(y))) (*)

Then

∀x (∃y (H(y,x) ˄ G(y)) ⇒ F(x))

is indeed equivalent to (*) because it is the contraposition of (*).