How would one prove that ∀a(P((a) v ∃bP(b)) is logically equivalent to ∃aP(a)? I am struggling to prove that

$\forall a (P(a) \vee \exists b P(b))$ is logically equivalent to $\exists a P(a)$


Here is my attempt to prove it:

~(∀a(P(a) ∨ ∃bP(b)) = ∃aP(a) 
  ~∃a~(P(a) v ∃bP(b)) = ∃aP(a) 
  ~∃a~P(a) and ~∀b~P(b)) = ∃aP(a) 
  therefore ~∃a~P(a) and ~∀b~P(b)) =/= ∃aP(a)

Is there any method to prove this aside from rules of inference and truth tables?
Can anyone give me some kind of help?
 A: What you did isn't getting you any closer ... 
Also, you should start with the LHS and eventually end up with the RHS: that's much more readable, and less subject to accidental circular reasoning, then what you did.
Now, it is not clear that you can actually do this one using purely equivalence rules anyway, but here is something you can do that approximates it (and is in fact a bit of a mix of a syntactical and semantical proof).
If $a,b,c,...$ denote the objects in your domain, then you can think of an existential like this:
$$\exists x \: \varphi(x) \approx \varphi(a) \lor \varphi(b) \lor \varphi(c) \lor ...$$
and likewise, a universal can be thought of as:
$$\forall x \: \varphi(x) \approx \varphi(a) \land \varphi(b) \land \varphi(c) \land ...$$ 
So now we can do:
$$\forall x (P(x) \lor \exists y \ P(y)) \approx$$
$$(P(a) \lor \exists y \ P(y)) \land (P(b) \lor \exists y \ P(y)) \land (P(c) \lor \exists y \ P(y)) \land... \Leftrightarrow \text{ (Distribution)}$$
$$(P(a) \land P(b) \land P(c) \land ... ) \lor \exists y \ P(y) \approx$$
$$(P(a) \land P(b) \land P(c) \land ... ) \lor P(a) \lor P(b) \lor P(c) \lor ...  \Leftrightarrow \text{ (Absorption)}$$
$$P(a) \lor P(b) \lor P(c) \lor ...  \approx$$
$$\exists x \ P(x)$$ 
The alternative would be to do a formal proof using rules of inference, rather than equivalence, as suggested in the comments.
A: Here's a proof using a Fitch-style proof checker:


As Graham Kemp mentioned in the comments below, I did not prove what the OP requested. The OP wanted a proof for the following:
$$
\forall x(Px \lor \exists y Py)\leftrightarrow \exists x Px
$$
Here is that proof:


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
