HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem grpideu 10976
Description: The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by Mario Carneiro, 8-Dec-2014.)
Hypotheses
Ref Expression
grpcl.b
grpcl.p
grpinvex.p
Assertion
Ref Expression
grpideu
Distinct variable groups:   ,,   ,,   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem grpideu
StepHypRef Expression
1 grpmnd 10972 . 2
2 grpcl.b . . 3
3 grpcl.p . . 3
42, 3mndideu 10915 . 2
51, 4syl 15 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   wceq 1414   wcel 1416  wral 2127  wreu 2129  cfv 4046  (class class class)co 5032  cbs 10495   cplusg 10533  cmnd 10901  cgrp 10902  c0g 10903
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-sep 3491  ax-nul 3500  ax-pr 3560  ax-un 3836
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2329  df-sbc 2496  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-nul 2908  df-if 3015  df-sn 3092  df-pr 3093  df-op 3095  df-uni 3247  df-br 3397  df-opab 3450  df-xp 4048  df-cnv 4050  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fv 4062  df-ov 5034  df-mnd 10907  df-grp 10967
Copyright terms: Public domain