Theorem idvalriota

Description: The unique value of the group identity element. (Contributed by FL, 12-Dec-2009) (Revised by AV, 24-Aug-2026)

	Ref	Expression
Hypotheses	grpidval.b	$$⊢B={\mathrm{Base}}_G$$
	grpidval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	grpidval.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	idvalriota	$$⊢\underset{\dot{}}{0}=\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpidval.b	$$⊢B={\mathrm{Base}}_G$$
2		grpidval.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		grpidval.o	$$⊢\underset{\dot{}}{0}=0_G$$
4	1 2 3	grpidval	$$⊢\underset{\dot{}}{0}=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
5		df-riota	$$⊢\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)=\left(\iota e|\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)\right)$$
6	4 5	eqtr4i	$$⊢\underset{\dot{}}{0}=\left(\iota e\in B|\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$