Theorem mgmideud

Description: Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (Revised by AV, 18-Aug-2026)

	Ref	Expression
Hypothesis	mgmideud.e	$$⊢\phi \to \exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
Assertion	mgmideud	$$⊢\phi \to \exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgmideud.e	$$⊢\phi \to \exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
2		mgmidmo	$$⊢{\exists }^{*}u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
3		reu5	$$⊢\exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\leftrightarrow \left(\exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge {\exists }^{*}u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\right)$$
4	1 2 3	sylanblrc	$$⊢\phi \to \exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$