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

Theorem grpideu 10761
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 10757 . 2
2 grpcl.b . . 3
3 grpcl.p . . 3
42, 3mndideu 10722 . 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 4033  (class class class)co 5002  cbs 10303   cplusg 10338  cmnd 10708  cgrp 10709  c0g 10710
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 3479  ax-nul 3488  ax-pr 3548  ax-un 3823
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 2328  df-sbc 2495  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-nul 2905  df-sn 3089  df-pr 3090  df-op 3092  df-uni 3234  df-br 3384  df-opab 3438  df-xp 4035  df-cnv 4037  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fv 4049  df-ov 5004  df-mnd 10714  df-grp 10752
Copyright terms: Public domain