Metamath Proof Explorer


Theorem gidsn

Description: Obsolete as of 23-Jan-2020. Use mnd1id instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis ablsn.1 AV
Assertion gidsn GIdAAA=A

Proof

Step Hyp Ref Expression
1 ablsn.1 AV
2 1 grposnOLD AAAGrpOp
3 opex AAV
4 3 rnsnop ranAAA=A
5 4 eqcomi A=ranAAA
6 eqid GIdAAA=GIdAAA
7 5 6 grpoidcl AAAGrpOpGIdAAAA
8 elsni GIdAAAAGIdAAA=A
9 2 7 8 mp2b GIdAAA=A