Is this proof correct? (Proof Theory)

Question

Is this proof correct?

Use C rule to prove $$\vdash\exists xC(x)\to\exists x(B(x)\lor C(x))$$

Proof:

By hypothesis, $\exists xC(x)$

By the C rule, $C(c)$

By $C\vdash B\lor C,C(c)\lor B(c)$

By $\exists-introduction, \exists x(B(x)\lor C(x))$

By Deduction theorem, $\vdash\exists xC(x)\to\exists x(B(x)\lor C(x))$

Answer 1

Yes.   The steps and justifications are okay, and indeed clearly what is required.

$$\begin{split}\exists x~B(x)&\vdash \exists x~B(x)&\textsf{Assumption} \\\exists x~B(x)&\vdash B(c) & \textsf{C-rule / Existential elimination}\\ B(c)&\vdash B(c)\vee C(c) & \textsf{Disjunction introduction}\\B(c)\vee C(c)&\vdash \exists x~(B(x)\vee C(x)) & \textsf{Existential introduction}\\ \hline &\vdash \exists x~B(x)~\to~ \exists x~(B(x)\vee C(x))~~ & \textsf{Deduction / Conditional introduction}\end{split}$$