Equivalence in natural deduction in First-order logic Task
$\vdash \exists x (P(x)\lor Q(x)) \iff \exists xP(x) \lor \exists xQ(x) $
My answer
If we have $A \iff B$ then $A\vdash B$ and $B \vdash A$.
So I started trying to see if I could prove $B$ from $A$, but in my tests I couldn't prove that. Below is an image of my attempt.

Is this correct or am I missing a step here? Any help is appreciated, thanks!
Edit
Would it maybe be possible to replace the $?$ with $Q(u) \space\space\space \space \neg Q(u)$ which would result in $\bot$ and from there I could use RAA?
 A: Here's an outline (in words) of how you could approach proving that $LHS \vdash RHS$:
Suppose that $\exists x (P(x) \vee Q(x))$.  Then choose a witness $a$ for this existence statement, so that $P(a) \vee Q(a)$.  We then proceed using a proof by cases to show that $(\exists x P(x)) \vee (\exists x Q(x))$.  In the first case, if $P(a)$, then it immediately follows that $\exists x P(x)$, so we can conclude $(\exists x P(x)) \vee (\exists x Q(x))$.  Likewise, if $Q(a)$, then it immediately follows that $\exists x Q(x)$, so we can conclude $(\exists x P(x)) \vee (\exists x Q(x))$ in this case also. $\quad\square$
A: A derivation in natural deduction proving that $\exists x (P(x) \lor Q(x)) \vdash \exists x \, P(x) \lor \exists x \, Q(x)$: 
$$
\dfrac{\exists x (P(x) \lor Q(x)) \quad \dfrac{[P(x) \lor Q(x)]^*\quad \dfrac{\dfrac{[P(x)]^{**}}{\exists y \, P(y)}\exists_i}{\exists y P(y) \lor \exists z Q(z)}\lor_{i_R} \quad \dfrac{\dfrac{[Q(x)]^{**}}{\exists z \, Q(z)}\exists_i}{\exists y P(y) \lor \exists z Q(z)}\lor_{i_L}}{\exists y \, P(y) \lor \exists z \, Q(z)}\lor_e^{**}}{\exists y \, P(y) \lor \exists z \, Q(z)}\exists_e^*
$$
The other direction is quite similar: the last rule of the derivation is a $\lor_e$ whose minor premises are conclusions of $\exists_e$.
In both directions there is no need for RAA.
A: If there is something that satisfies P or Q, then there is a case for something satisfying P or there is a case for something satisfying Q.
$$\dfrac{\dfrac{\dfrac{[\exists x~(P(x)\vee Q(x))]^1}{a:P(a)\vee Q(a)}~\dfrac{\dfrac{[a:P(a)]^2}{\phantom{\exists x~P(x)}}}{\phantom{\exists x~P(x)~\vee~\exists x~Q(x)}}~\dfrac{\dfrac{[a:Q(a)]^2}{\phantom{\exists x~Q(x)}}}{\phantom{\exists x~P(x)~\vee~\exists x~Q(x)}}}{{\exists x~P(x)~\vee~\exists x~Q(x)}}{^2}}{\exists x~(P(x)\vee Q(x))~\to~(\exists x~P(x)~\vee~\exists x~Q(x))}{^1}$$

If there is something that satisfies P then there is something satisfying P or Q.  If there is something that satisfies Q then there is something satisfying P or Q.  In either case the conclusion holds.
$$\dfrac{\dfrac{\lower{8ex}{[\exists x~P(x)~\vee~\exists x~Q(x)]^1}~\dfrac{[\exists x~P(x)]^2}{\dfrac{\phantom{a:P(a)}}{\dfrac{\phantom{a:P(a)\vee Q(a)}}{\phantom{\exists x~(P(x)\vee Q(x))}}}}~\dfrac{[\exists x~Q(x)]^2}{\dfrac{\phantom{a:Q(a)}}{\dfrac{\phantom{a:P(a)\vee Q(a)}}{\phantom{\exists x~(P(x)\vee Q(x))}}}}}{\exists x~(P(x)\vee Q(x))}{^2}}{(\exists x~P(x)~\vee~\exists x~ Q(x))~\to~\exists x~(P(x)\vee Q(x))}{^1}$$
