Te estás haciendo un lío importante con la lógica, me parece a mí.
Veamos, lo primero es que esto:
\[ [(\exists e\in A\,\forall x\in A:x*e=e*x=x)\land B\subseteq A\color{red}\land\exists e'\in B\,\forall x'\in B\color{black}]\to(x'*e'=e'*x'=x') \]
no tiene ningún sentido. No es una fórmula bien formada, no significa nada en lógica de primer orden. Detrás de un cuantificador siempre debe ir otra fórmula, y no tiene ningún sentido partirlo. La verdad es que ahora entiendo por qué empezabas con un "Supongamos \[ \exists e \in B \]". Tanto Luis como yo hemos interpretado que querías decir "Supongamos que \[ \exists e (e \in B) \]" (es decir, \[ B \neq \emptyset \]) pero no, estabas suponiendo el principio de la fórmula \[ \exists e\in B \forall x \in B (e*x=x*e=x) \]. Pero esto, ¡no tiene ningún sentido! Las fórmulas no se parten así. Si quieres demostrar una fórmula del tipo \[ \exists e \in B \phi(e) \] lo que debes hacer es encontrar un elemento específico \[ e \in B \] que cumpla \[ \phi(e) \], no suponer \[ \exists e\in B \] (que por sí solo no tiene ningún sentido) y a partir de ahí demostrar \[ e \in B \].
Otra cosa: los dos puntitos : en la fórmula
\[ [(\exists e\in A\,\forall x\in A:x*e=e*x=x)\land B\subseteq A]\to(\exists e'\in B\,\forall x'\in B:x'*e'=e'*x'=x') \]
no significan absolutamente nada, es lo mismo que escribir
\[ [(\exists e\in A\,\forall x\in A(x*e=e*x=x))\land B\subseteq A]\to(\exists e'\in B\,\forall x'\in B(x'*e'=e'*x'=x')) \]
o directamente
\[ [(\exists e\in A\,\forall x\in A\; x*e=e*x=x)\land B\subseteq A]\to(\exists e'\in B\,\forall x'\in B \; x'*e'=e'*x'=x') \].
Son un recurso estético a la hora de escribir las fórmulas para separar el cuantificador de la fórmula que le sigue, pero no tiene ningún significado a nivel lógico o matemático. Lo que sí te tiene que quedar claro es que no son un implicador ni tienen nada que ver con implicadores.
Entonces, un supuesto intento de demostración (más o menos formal) de
\[ [(\exists e\in A\,\forall x\in A:x*e=e*x=x)\land B\subseteq A]\to(\exists e'\in B\,\forall x'\in B:x'*e'=e'*x'=x') \]
empezaría así:
Supongamos \[ (\exists e\in A\,\forall x\in A:x*e=e*x=x)\land B\subseteq A \], y queremos demostrar \[ (\exists e'\in B\,\forall x'\in B:x'*e'=e'*x'=x') \]. Tenemos pues que \[ \exists e\in A\,\forall x\in A:x*e=e*x=x \] y que \[ B \subseteq A \]. Como \[ \exists e\in A\,\forall x\in A:x*e=e*x=x \] (que es lo que estamos suponiendo) empieza por un existencial, podemos particularizar, es decir, tenemos un elemento \[ e \in A \] que cumple \[ \forall x\in A:x*e=e*x=x \]. Si \[ x \in B \], como \[ B \subseteq A \], también tenemos que \[ x \in A \]. En particular, \[ x*e=e*x=x \]. Luego tenemos \[ \forall x\in B:x*e=e*x=x \]. Parecería que estamos cerca, solamente faltaría probar que \[ e \in B \] para concluir que \[ \exists e\in B \forall x\in B:x*e=e*x=x \]. Pero eso no se puede hacer porque es falso en general. Otro camino sería intentar encontrar otro elemento \[ e' \in B \] que fuera el neutro de \[ B \], pero no hay una elección obvia para \[ e' \] distinta de \[ e \] (y de hecho en general es imposible porque la proposición es falsa). Así que llegamos a un punto muerto.
De todas formas, lo que ya te hemos dicho mil veces: no pienses las demostraciones como demostraciones formales, sintácticamente, en plan "quiero demostrar esta fórmula, supongo este trozo de aquí y voy a intentar probar este trozo de allá, etc" sin prestar atención al contenido. Es mucho mejor pensar semánticamente, es decir, pensar en términos de los objetos de los que habla la proposición, pensar en qué significa y si es cierto o no. Lo de las demostraciones formales es el mejor camino para que una chorrada se te complique hasta niveles estratosféricos, y más aún si no tienes del todo clara la sintaxis de la lógica de primer orden.
