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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpidval.p	⊢ + = ( +g ‘ 𝐺 )
	grpidval.o	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	idvalriota	⊢ 0 = ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		grpidval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpidval.p	⊢ + = ( +g ‘ 𝐺 )
3		grpidval.o	⊢ 0 = ( 0g ‘ 𝐺 )
4	1 2 3	grpidval	⊢ 0 = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
5		df-riota	⊢ ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
6	4 5	eqtr4i	⊢ 0 = ( ℩ 𝑒 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) )