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 A V
Assertion gidsn GId A A A = A


Step Hyp Ref Expression
1 ablsn.1 A V
2 1 grposnOLD A A A GrpOp
3 opex A A V
4 3 rnsnop ran A A A = A
5 4 eqcomi A = ran A A A
6 eqid GId A A A = GId A A A
7 5 6 grpoidcl A A A GrpOp GId A A A A
8 elsni GId A A A A GId A A A = A
9 2 7 8 mp2b GId A A A = A