Let $\mathcal{L}=\{e,f\}$ where $e$ is a constant symbol and $f$ is a 2-arity function symbol. Consider the group's theory axioms: $$\varphi_1 : \forall x \forall y \forall z (fxfyz=ffxyz)$$
$$\varphi_2 : \forall x (fex=x \land fxe=x)$$
$$\varphi_3 : \forall x \exists y (fxy=e \land fyx=e) $$
and the set of all of them: $\Sigma := \{\varphi_1, \varphi_2, \varphi_3 \}$
I have to make a proof of: $\Sigma \vdash \forall x (fex=e \rightarrow x=e)$ with the Mileti's book "A mathematical introduction to mathematical logic" rules for syntactic implication on first-order-logic.
I wrote the following posible answer and I want to know if it is correct:
$$\begin{matrix} \forall x (fex=x \land fxe=x) \vdash \forall x (fex=x \land fxe=x) \hspace{1cm} & (Assume) \text{ on } \varphi_2 & (1) \\ \forall x (fex=x \land fxe=x) \vdash fey=y \land fye=y & (\forall E) \text{ on } (1) & (2) \\ \forall x (fex=x \land fxe=x) \vdash fey=y & (\land EL) \text{ on } (2) & (3) \\ \forall x (fex=x \land fxe=x), fey=e \vdash fey=y & (Expand) \text{ on } (3) & (4) \\ fey=e \vdash fey=e & (Assume) & (5) \\ fey=e, \forall x (fex=x \land fxe=x) \vdash fey=e & (Expand) \text{ on } (5) & (6) \\ \forall x (fex=x \land fxe=x), fey=e \vdash fey=e & (Reorder) \text{ on } (6) & (7) \\ \forall x (fex=x \land fxe=x), fey=e \vdash y=e & (=Sub) \text{ on } (4), (7) & (8) \\ \forall x (fex=x \land fxe=x) \vdash fey=e \rightarrow y=e & (\rightarrow I) \text{ on } (8) & (9) \\ \forall x (fex=x \land fxe=x) \vdash \forall x (fex=e \rightarrow x=e) & (\forall I) \text{ on } (9) & (10) \end{matrix}$$
Since $\varphi_2 \in \Sigma$, it follows that $\Sigma \vdash \forall x (fex=e \rightarrow x=e)$.