Formal proof with first order logic axioms.

Question

How do I formally prove the following:

$$[\forall y Gy \wedge \exists x Hx] \iff \exists x[\forall y Gy \wedge Hx]$$

and by formally I mean using premises and whatever other first order logical axioms are needed.

I proved it like such, but this is not how I was supposed to do it.

$[\forall y Gy \wedge \exists x Hx] \iff \exists x[\forall y Gy \wedge Hx]$ : Distribute Quantifier

$\implies$ $[\forall y Gy \wedge \exists x Hx] \iff [\forall x\forall y Gy \wedge \exists x Hx]$ :Null Quantification

$\implies$ $[\forall y Gy \wedge \exists x Hx] \iff [\forall y Gy \wedge \exists x Hx]$

Can anyone help? Here are some of the Axioms accepted:

$$M.P: Modus Ponens$$

$$TA : Tautologies$$

$$\forall x(\delta \implies \psi) \implies (\forall x\delta \implies \forall x\psi)$$

$$E.I: Existential Instantiation$$ $$U.G: Universal Generalization$$ $$U.I: Universal Instantiation$$ $$E.G: Existential Generalization$$

Answer 1

Here's a proof that I think complies with your rules.

Answer 2

I see you were trying Quantifier Distribution and null Quantification so I assume it is ok to use equivalence rules.

Well, this is an immediate application of a Prenex Law:

$Q \land \exists x \phi(x) \Leftrightarrow \exists x (Q \land \phi(x))$

Where Q does not contain $x$ as a free variable.

If equivalence rules are not allowed, then we will need to know what inference rules you are allowed.