Theorem grpidcl 13836

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

Hypotheses

Ref	Expression
grpidcl.b	⊢ 𝐵 = (Base‘𝐺)
grpidcl.o	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
grpidcl	⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)

Proof of Theorem grpidcl

Step	Hyp	Ref	Expression
1		grpmnd 13814	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpidcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpidcl.o	. . 3 ⊢ 0 = (0g‘𝐺)
4	2, 3	mndidcl 13745	. 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
5	1, 4	syl 14	1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  ‘cfv 5377  Basecbs 13354  0_gc0g 13612  Mndcmnd 13731  Grpcgrp 13807

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-iota 5337  df-fun 5379  df-fn 5380  df-fv 5385  df-riota 6038  df-ov 6088  df-inn 9306  df-2 9364  df-ndx 13357  df-slot 13358  df-base 13360  df-plusg 13446  df-0g 13614  df-mgm 13678  df-sgrp 13719  df-mnd 13732  df-grp 13810

This theorem is used by:  grpbn0  13837  grprcan  13844  grpid  13846  isgrpid2  13847  grprinv  13858  grpidinv  13866  grpinvid  13867  grpressid  13868  grpidrcan  13872  grpidlcan  13873  grpidssd  13883  grpinvval2  13890  grpsubid1  13892  dfgrp3m  13906  grpsubpropd2  13912  imasgrp  13916  mulgcl  13944  mulgz  13955  subg0  13985  subg0cl  13987  issubg2m  13994  issubg4m  13998  grpissubg  13999  subgintm  14003  0subg  14004  nmzsubg  14015  0nsg  14019  triv1nsgd  14023  eqgid  14031  eqg0el  14034  qusgrp  14037  qus0  14040  ghmid  14054  ghmrn  14062  ghmpreima  14071  f1ghm0to0  14077  kerf1ghm  14079  rng0cl  14244  rnglz  14246  rngrz  14247  ring0cl  14328  ringlz  14350  ringrz  14351  aprlring  14602  lmod0vcl  14656  lmodfopnelem1  14663  rmodislmodlem  14689  rmodislmod  14690  islss3  14718  ascl0  15029  psr0cl  15074  psr0lid  15075  mplsubgfilemm  15091