Metamath Proof Explorer


Theorem grpidcl

Description: The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses grpidcl.b B=BaseG
grpidcl.o 0˙=0G
Assertion grpidcl GGrp0˙B

Proof

Step Hyp Ref Expression
1 grpidcl.b B=BaseG
2 grpidcl.o 0˙=0G
3 grpmnd GGrpGMnd
4 1 2 mndidcl GMnd0˙B
5 3 4 syl GGrp0˙B